English
Coherence identity: t'(𝒰) i j k ≫ snd ≫ snd = fst ≫ fst ≫ fst, expressing triple overlap compatibility.
Русский
Когерентное тождество: t'(𝒰) i j k ≫ snd ≫ snd = fst ≫ fst ≫ fst, выражающее совместимость на тройном перекрытии.
LaTeX
$$$ t'_{\\mathcal{U}} f g i j k \\;\\gg\\; \\mathrm{snd} \\_ \\_ \\;\\gg\\; \\mathrm{snd} \\_ \\_ = \\mathrm{fst} \\_ \\_ \\;\\gg\\; \\mathrm{fst} \\_ \\_ \\;\\gg\\; \\mathrm{fst} \\_ \\_$$
Lean4
@[simp, reassoc]
theorem t'_snd_snd (i j k : 𝒰.I₀) :
t' 𝒰 f g i j k ≫ pullback.snd _ _ ≫ pullback.snd _ _ = pullback.fst _ _ ≫ pullback.fst _ _ ≫ pullback.fst _ _ := by
simp only [t', Category.assoc, pullbackSymmetry_hom_comp_snd_assoc, pullbackRightPullbackFstIso_inv_fst_assoc,
pullback.lift_fst_assoc, t_snd, pullbackRightPullbackFstIso_hom_fst_assoc]
