English
Under the same assumptions, for all i, j, k, the relation t'(𝒰) i j k ≫ fst ≫ snd = fst ≫ fst ≫ snd holds, expressing another coherence of the pullback data.
Русский
При тех же предпосылках для любых i, j, k выполняется отношение t'(𝒰) i j k ≫ fst ≫ snd = fst ≫ fst ≫ snd, выражающее другую когерентность данных обратного диаграммы.
LaTeX
$$$ t'_{\\mathcal{U}} f g i j k \\;\\gg\\; \\mathrm{fst} \\_ \\_ \\;\\gg\\; \\mathrm{snd} \\_ \\_ = \\mathrm{fst} \\_ \\_ \\;\\gg\\; \\mathrm{fst} \\_ \\_ \\;\\gg\\; \\mathrm{snd} \\_ \\_$$
Lean4
@[simp, reassoc]
theorem t'_fst_snd (i j k : 𝒰.I₀) :
t' 𝒰 f g i j k ≫ pullback.fst _ _ ≫ pullback.snd _ _ = pullback.snd _ _ ≫ pullback.snd _ _ := by
simp only [t', Category.assoc, pullbackSymmetry_hom_comp_fst_assoc, pullbackRightPullbackFstIso_inv_snd_snd,
pullback.lift_snd, Category.comp_id, pullbackRightPullbackFstIso_hom_snd]
