English
The Map construction respects composition: the composition of maps between equalizers equals the map of composed maps with the appropriate square data.
Русский
Конструкция Map сохраняет композицию: композиция отображений между равноподобиями равна отображению произведённых отображений с нужными данными квадратов.
LaTeX
$$$(\\operatorname{map} \\phi' \\psi' hf' hg') \\circ (\\operatorname{map} \\phi \\psi hf hg) = \\operatorname{map} (\\phi' \\circ \\phi) (\\psi' \\circ \\psi) (comm\_sq_2 hf hf') (comm\_sq_2 hg hg')$$$
Lean4
theorem map_comp_map (hf : ψ.comp f₁ = f₂.comp φ) (hg : ψ.comp g₁ = g₂.comp φ) (hf' : ψ'.comp f₂ = f₃.comp φ')
(hg' : ψ'.comp g₂ = g₃.comp φ') :
(map φ' ψ' hf' hg').comp (map φ ψ hf hg) = map (φ'.comp φ) (ψ'.comp ψ) (comm_sq₂ hf hf') (comm_sq₂ hg hg') :=
by
ext
rfl
