English
Let F: C → D be a functor, d ∈ D, and f1, f2 in Σ X, d ⟶ F.obj X. If t is a witness that f1 and f2 are related by the equivalence relation EqvGen generated by the ColimitTypeRel(F ⋙ coyoneda.obj(op d)), then there exists a zigzag in the StructuredArrow from f1.2 to f2.2.
Русский
Пусть F: C → D. Пусть d ∈ D и f1, f2 ∈ Σ X, d ⟶ F.obj X. Если t является доказательством того, что f1 и f2 связаны эквивалентностью EqvGen, порожденной rel(F ⋙ coyoneda.obj(op d)), то существует зигзаг в категори StructuredArrow от f1.2 к f2.2.
LaTeX
$$$\\forall d\\in D,\\; f_1,f_2:\\Sigma X, d \\to F.obj X,\\; t \\in \\mathrm{Relation.EqvGen}(\\mathrm{Functor.ColimitTypeRel}(F \\circ \\mathrm{coyoneda.obj}(\\mathrm{op} \\\\ d)))\\; f_1 f_2 \\Rightarrow \\mathrm{Zigzag}(\\mathrm{StructuredArrow.mk} f_1.2)(\\mathrm{StructuredArrow.mk} f_2.2).$$
Lean4
theorem zigzag_of_eqvGen_colimitTypeRel {F : C ⥤ D} {d : D} {f₁ f₂ : Σ X, d ⟶ F.obj X}
(t : Relation.EqvGen (Functor.ColimitTypeRel (F ⋙ coyoneda.obj (op d))) f₁ f₂) :
Zigzag (StructuredArrow.mk f₁.2) (StructuredArrow.mk f₂.2) := by
induction t with
| rel x y r =>
obtain ⟨f, w⟩ := r
fconstructor
swap
· fconstructor
left; fconstructor
exact StructuredArrow.homMk f
| refl => fconstructor
| symm x y _ ih =>
apply zigzag_symmetric
exact ih
| trans x y z _ _ ih₁ ih₂ =>
apply Relation.ReflTransGen.trans
· exact ih₁
· exact ih₂
