English
Similar coherence identity involving snd, fst, fst, namely t'(𝒰) i j k ≫ snd ≫ fst ≫ fst = fst ≫ fst ≫ snd.
Русский
Подобное когерентное тождество с участием snd, fst, fst: t'(𝒰) i j k ≫ snd ≫ fst ≫ fst = fst ≫ fst ≫ snd.
LaTeX
$$$ t'_{\\mathcal{U}} f g i j k \\;\\gg\\; \\mathrm{snd} \\_ \\_ \\;\\gg\\; \\mathrm{fst} \\_ \\_ \\;\\gg\\; \\mathrm{fst} \\_ \\_ = \\mathrm{fst} \\_ \\_ \\;\\gg\\; \\mathrm{fst} \\_ \\_ \\;\\gg\\; \\mathrm{snd} \\_ \\_$$
Lean4
@[simp, reassoc]
theorem t'_snd_fst_fst (i j k : 𝒰.I₀) :
t' 𝒰 f g i j k ≫ pullback.snd _ _ ≫ pullback.fst _ _ ≫ pullback.fst _ _ = pullback.fst _ _ ≫ pullback.snd _ _ := by
simp only [t', Category.assoc, pullbackSymmetry_hom_comp_snd_assoc, pullbackRightPullbackFstIso_inv_fst_assoc,
pullback.lift_fst_assoc, t_fst_fst, pullbackRightPullbackFstIso_hom_fst_assoc]
