C : Type v
inst✝² : Category C
D : Type v
inst✝¹ : Category D
F : C ⥤ D
inst✝ : Final F
I : (d : D) → colimit (F ⋙ coyoneda.obj d.op) ≅ PUnit
d : D
this : Nonempty (StructuredArrow d F)
⊢ IsConnected (StructuredArrow d F)
C : Type v
inst✝² : Category C
D : Type v
inst✝¹ : Category D
F : C ⥤ D
inst✝ : Final F
I : (d : D) → colimit (F ⋙ coyoneda.obj d.op) ≅ PUnit
d : D
⊢ IsConnected (StructuredArrow d F)
have : Nonempty (StructuredArrow d F) := by
  have := (I d).inv PUnit.unit
  obtain ⟨j, y, rfl⟩ := Limits.Types.jointly_surjective'.{v, v} this
  exact ⟨StructuredArrow.mk y⟩
case h
C : Type v
inst✝² : Category C
D : Type v
inst✝¹ : Category D
F : C ⥤ D
inst✝ : Final F
I : (d : D) → colimit (F ⋙ coyoneda.obj d.op) ≅ PUnit
d : D
this : Nonempty (StructuredArrow d F)
⊢ ∀ (j₁ j₂ : StructuredArrow d F), Zigzag j₁ j₂
C : Type v
inst✝² : Category C
D : Type v
inst✝¹ : Category D
F : C ⥤ D
inst✝ : Final F
I : (d : D) → colimit (F ⋙ coyoneda.obj d.op) ≅ PUnit
d : D
this : Nonempty (StructuredArrow d F)
⊢ IsConnected (StructuredArrow d F)
apply zigzag_isConnected
case h.mk.mk.unit.mk.mk.unit
C : Type v
inst✝² : Category C
D : Type v
inst✝¹ : Category D
F : C ⥤ D
inst✝ : Final F
I : (d : D) → colimit (F ⋙ coyoneda.obj d.op) ≅ PUnit
d : D
this : Nonempty (StructuredArrow d F)
X₁ : C
f₁ : (fromPUnit d).obj { as := PUnit.unit } ⟶ F.obj X₁
X₂ : C
f₂ : (fromPUnit d).obj { as := PUnit.unit } ⟶ F.obj X₂
⊢ Zigzag { left := { as := PUnit.unit }, right := X₁, hom := f₁ }
    { left := { as := PUnit.unit }, right := X₂, hom := f₂ }
case h
C : Type v
inst✝² : Category C
D : Type v
inst✝¹ : Category D
F : C ⥤ D
inst✝ : Final F
I : (d : D) → colimit (F ⋙ coyoneda.obj d.op) ≅ PUnit
d : D
this : Nonempty (StructuredArrow d F)
⊢ ∀ (j₁ j₂ : StructuredArrow d F), Zigzag j₁ j₂
rintro ⟨⟨⟨⟩⟩, X₁, f₁⟩ ⟨⟨⟨⟩⟩, X₂, f₂⟩
case h.mk.mk.unit.mk.mk.unit
C : Type v
inst✝² : Category C
D : Type v
inst✝¹ : Category D
F : C ⥤ D
inst✝ : Final F
I : (d : D) → colimit (F ⋙ coyoneda.obj d.op) ≅ PUnit
d : D
this : Nonempty (StructuredArrow d F)
X₁ : C
f₁ : (fromPUnit d).obj { as := PUnit.unit } ⟶ F.obj X₁
X₂ : C
f₂ : (fromPUnit d).obj { as := PUnit.unit } ⟶ F.obj X₂
⊢ Zigzag { left := { as := PUnit.unit }, right := X₁, hom := f₁ }
    { left := { as := PUnit.unit }, right := X₂, hom := f₂ }
case h.mk.mk.unit.mk.mk.unit
C : Type v
inst✝² : Category C
D : Type v
inst✝¹ : Category D
F : C ⥤ D
inst✝ : Final F
I : (d : D) → colimit (F ⋙ coyoneda.obj d.op) ≅ PUnit
d : D
this : Nonempty (StructuredArrow d F)
X₁ : C
f₁ : (fromPUnit d).obj { as := PUnit.unit } ⟶ F.obj X₁
X₂ : C
f₂ : (fromPUnit d).obj { as := PUnit.unit } ⟶ F.obj X₂
⊢ Zigzag { left := { as := PUnit.unit }, right := X₁, hom := f₁ }
    { left := { as := PUnit.unit }, right := X₂, hom := f₂ }
dsimp at *
case h.mk.mk.unit.mk.mk.unit
C : Type v
inst✝² : Category C
D : Type v
inst✝¹ : Category D
F : C ⥤ D
inst✝ : Final F
I : (d : D) → colimit (F ⋙ coyoneda.obj d.op) ≅ PUnit
d : D
this : Nonempty (StructuredArrow d F)
X₁ : C
f₁ : (fromPUnit d).obj { as := PUnit.unit } ⟶ F.obj X₁
X₂ : C
f₂ : (fromPUnit d).obj { as := PUnit.unit } ⟶ F.obj X₂
y₁ : colimit (F ⋙ coyoneda.obj d.op) := colimit.ι (F ⋙ coyoneda.obj d.op) X₁ f₁
⊢ Zigzag { left := { as := PUnit.unit }, right := X₁, hom := f₁ }
    { left := { as := PUnit.unit }, right := X₂, hom := f₂ }
case h.mk.mk.unit.mk.mk.unit
C : Type v
inst✝² : Category C
D : Type v
inst✝¹ : Category D
F : C ⥤ D
inst✝ : Final F
I : (d : D) → colimit (F ⋙ coyoneda.obj d.op) ≅ PUnit
d : D
this : Nonempty (StructuredArrow d F)
X₁ : C
f₁ : (fromPUnit d).obj { as := PUnit.unit } ⟶ F.obj X₁
X₂ : C
f₂ : (fromPUnit d).obj { as := PUnit.unit } ⟶ F.obj X₂
⊢ Zigzag { left := { as := PUnit.unit }, right := X₁, hom := f₁ }
    { left := { as := PUnit.unit }, right := X₂, hom := f₂ }
let y₁ := colimit.ι (F ⋙ coyoneda.obj (op d)) X₁ f₁
case h.mk.mk.unit.mk.mk.unit
C : Type v
inst✝² : Category C
D : Type v
inst✝¹ : Category D
F : C ⥤ D
inst✝ : Final F
I : (d : D) → colimit (F ⋙ coyoneda.obj d.op) ≅ PUnit
d : D
this : Nonempty (StructuredArrow d F)
X₁ : C
f₁ : (fromPUnit d).obj { as := PUnit.unit } ⟶ F.obj X₁
X₂ : C
f₂ : (fromPUnit d).obj { as := PUnit.unit } ⟶ F.obj X₂
y₁ : colimit (F ⋙ coyoneda.obj d.op) := colimit.ι (F ⋙ coyoneda.obj d.op) X₁ f₁
y₂ : colimit (F ⋙ coyoneda.obj d.op) := colimit.ι (F ⋙ coyoneda.obj d.op) X₂ f₂
⊢ Zigzag { left := { as := PUnit.unit }, right := X₁, hom := f₁ }
    { left := { as := PUnit.unit }, right := X₂, hom := f₂ }
case h.mk.mk.unit.mk.mk.unit
C : Type v
inst✝² : Category C
D : Type v
inst✝¹ : Category D
F : C ⥤ D
inst✝ : Final F
I : (d : D) → colimit (F ⋙ coyoneda.obj d.op) ≅ PUnit
d : D
this : Nonempty (StructuredArrow d F)
X₁ : C
f₁ : (fromPUnit d).obj { as := PUnit.unit } ⟶ F.obj X₁
X₂ : C
f₂ : (fromPUnit d).obj { as := PUnit.unit } ⟶ F.obj X₂
y₁ : colimit (F ⋙ coyoneda.obj d.op) := colimit.ι (F ⋙ coyoneda.obj d.op) X₁ f₁
⊢ Zigzag { left := { as := PUnit.unit }, right := X₁, hom := f₁ }
    { left := { as := PUnit.unit }, right := X₂, hom := f₂ }
let y₂ := colimit.ι (F ⋙ coyoneda.obj (op d)) X₂ f₂
case h.mk.mk.unit.mk.mk.unit
C : Type v
inst✝² : Category C
D : Type v
inst✝¹ : Category D
F : C ⥤ D
inst✝ : Final F
I : (d : D) → colimit (F ⋙ coyoneda.obj d.op) ≅ PUnit
d : D
this : Nonempty (StructuredArrow d F)
X₁ : C
f₁ : (fromPUnit d).obj { as := PUnit.unit } ⟶ F.obj X₁
X₂ : C
f₂ : (fromPUnit d).obj { as := PUnit.unit } ⟶ F.obj X₂
y₁ : colimit (F ⋙ coyoneda.obj d.op) := colimit.ι (F ⋙ coyoneda.obj d.op) X₁ f₁
y₂ : colimit (F ⋙ coyoneda.obj d.op) := colimit.ι (F ⋙ coyoneda.obj d.op) X₂ f₂
e : y₁ = y₂
⊢ Zigzag { left := { as := PUnit.unit }, right := X₁, hom := f₁ }
    { left := { as := PUnit.unit }, right := X₂, hom := f₂ }
case h.mk.mk.unit.mk.mk.unit
C : Type v
inst✝² : Category C
D : Type v
inst✝¹ : Category D
F : C ⥤ D
inst✝ : Final F
I : (d : D) → colimit (F ⋙ coyoneda.obj d.op) ≅ PUnit
d : D
this : Nonempty (StructuredArrow d F)
X₁ : C
f₁ : (fromPUnit d).obj { as := PUnit.unit } ⟶ F.obj X₁
X₂ : C
f₂ : (fromPUnit d).obj { as := PUnit.unit } ⟶ F.obj X₂
y₁ : colimit (F ⋙ coyoneda.obj d.op) := colimit.ι (F ⋙ coyoneda.obj d.op) X₁ f₁
y₂ : colimit (F ⋙ coyoneda.obj d.op) := colimit.ι (F ⋙ coyoneda.obj d.op) X₂ f₂
⊢ Zigzag { left := { as := PUnit.unit }, right := X₁, hom := f₁ }
    { left := { as := PUnit.unit }, right := X₂, hom := f₂ }
have e : y₁ = y₂ := by
  apply (I d).toEquiv.injective
  ext
case h.mk.mk.unit.mk.mk.unit
C : Type v
inst✝² : Category C
D : Type v
inst✝¹ : Category D
F : C ⥤ D
inst✝ : Final F
I : (d : D) → colimit (F ⋙ coyoneda.obj d.op) ≅ PUnit
d : D
this : Nonempty (StructuredArrow d F)
X₁ : C
f₁ : (fromPUnit d).obj { as := PUnit.unit } ⟶ F.obj X₁
X₂ : C
f₂ : (fromPUnit d).obj { as := PUnit.unit } ⟶ F.obj X₂
y₁ : colimit (F ⋙ coyoneda.obj d.op) := colimit.ι (F ⋙ coyoneda.obj d.op) X₁ f₁
y₂ : colimit (F ⋙ coyoneda.obj d.op) := colimit.ι (F ⋙ coyoneda.obj d.op) X₂ f₂
e : y₁ = y₂
t : EqvGen (Types.Quot.Rel (F ⋙ coyoneda.obj d.op)) { fst := X₁, snd := f₁ } { fst := X₂, snd := f₂ }
⊢ Zigzag { left := { as := PUnit.unit }, right := X₁, hom := f₁ }
    { left := { as := PUnit.unit }, right := X₂, hom := f₂ }
case h.mk.mk.unit.mk.mk.unit
C : Type v
inst✝² : Category C
D : Type v
inst✝¹ : Category D
F : C ⥤ D
inst✝ : Final F
I : (d : D) → colimit (F ⋙ coyoneda.obj d.op) ≅ PUnit
d : D
this : Nonempty (StructuredArrow d F)
X₁ : C
f₁ : (fromPUnit d).obj { as := PUnit.unit } ⟶ F.obj X₁
X₂ : C
f₂ : (fromPUnit d).obj { as := PUnit.unit } ⟶ F.obj X₂
y₁ : colimit (F ⋙ coyoneda.obj d.op) := colimit.ι (F ⋙ coyoneda.obj d.op) X₁ f₁
y₂ : colimit (F ⋙ coyoneda.obj d.op) := colimit.ι (F ⋙ coyoneda.obj d.op) X₂ f₂
e : y₁ = y₂
⊢ Zigzag { left := { as := PUnit.unit }, right := X₁, hom := f₁ }
    { left := { as := PUnit.unit }, right := X₂, hom := f₂ }
have t := Types.colimit_eq.{v, v} e
case h.mk.mk.unit.mk.mk.unit
C : Type v
inst✝² : Category C
D : Type v
inst✝¹ : Category D
F : C ⥤ D
inst✝ : Final F
I : (d : D) → colimit (F ⋙ coyoneda.obj d.op) ≅ PUnit
d : D
this : Nonempty (StructuredArrow d F)
X₁ : C
f₁ : (fromPUnit d).obj { as := PUnit.unit } ⟶ F.obj X₁
X₂ : C
f₂ : (fromPUnit d).obj { as := PUnit.unit } ⟶ F.obj X₂
t : EqvGen (Types.Quot.Rel (F ⋙ coyoneda.obj d.op)) { fst := X₁, snd := f₁ } { fst := X₂, snd := f₂ }
⊢ Zigzag { left := { as := PUnit.unit }, right := X₁, hom := f₁ }
    { left := { as := PUnit.unit }, right := X₂, hom := f₂ }
case h.mk.mk.unit.mk.mk.unit
C : Type v
inst✝² : Category C
D : Type v
inst✝¹ : Category D
F : C ⥤ D
inst✝ : Final F
I : (d : D) → colimit (F ⋙ coyoneda.obj d.op) ≅ PUnit
d : D
this : Nonempty (StructuredArrow d F)
X₁ : C
f₁ : (fromPUnit d).obj { as := PUnit.unit } ⟶ F.obj X₁
X₂ : C
f₂ : (fromPUnit d).obj { as := PUnit.unit } ⟶ F.obj X₂
y₁ : colimit (F ⋙ coyoneda.obj d.op) := colimit.ι (F ⋙ coyoneda.obj d.op) X₁ f₁
y₂ : colimit (F ⋙ coyoneda.obj d.op) := colimit.ι (F ⋙ coyoneda.obj d.op) X₂ f₂
e : y₁ = y₂
t : EqvGen (Types.Quot.Rel (F ⋙ coyoneda.obj d.op)) { fst := X₁, snd := f₁ } { fst := X₂, snd := f₂ }
⊢ Zigzag { left := { as := PUnit.unit }, right := X₁, hom := f₁ }
    { left := { as := PUnit.unit }, right := X₂, hom := f₂ }
clear e y₁ y₂
no goals
case h.mk.mk.unit.mk.mk.unit
C : Type v
inst✝² : Category C
D : Type v
inst✝¹ : Category D
F : C ⥤ D
inst✝ : Final F
I : (d : D) → colimit (F ⋙ coyoneda.obj d.op) ≅ PUnit
d : D
this : Nonempty (StructuredArrow d F)
X₁ : C
f₁ : (fromPUnit d).obj { as := PUnit.unit } ⟶ F.obj X₁
X₂ : C
f₂ : (fromPUnit d).obj { as := PUnit.unit } ⟶ F.obj X₂
t : EqvGen (Types.Quot.Rel (F ⋙ coyoneda.obj d.op)) { fst := X₁, snd := f₁ } { fst := X₂, snd := f₂ }
⊢ Zigzag { left := { as := PUnit.unit }, right := X₁, hom := f₁ }
    { left := { as := PUnit.unit }, right := X₂, hom := f₂ }
exact zigzag_of_eqvGen_quot_rel t
C : Type v
inst✝² : Category C
D : Type v
inst✝¹ : Category D
F : C ⥤ D
inst✝ : Final F
I : (d : D) → colimit (F ⋙ coyoneda.obj d.op) ≅ PUnit
d : D
this : colimit (F ⋙ coyoneda.obj d.op)
⊢ Nonempty (StructuredArrow d F)
C : Type v
inst✝² : Category C
D : Type v
inst✝¹ : Category D
F : C ⥤ D
inst✝ : Final F
I : (d : D) → colimit (F ⋙ coyoneda.obj d.op) ≅ PUnit
d : D
⊢ Nonempty (StructuredArrow d F)
have := (I d).inv PUnit.unit
case intro.intro
C : Type v
inst✝² : Category C
D : Type v
inst✝¹ : Category D
F : C ⥤ D
inst✝ : Final F
I : (d : D) → colimit (F ⋙ coyoneda.obj d.op) ≅ PUnit
d : D
j : C
y : (F ⋙ coyoneda.obj d.op).obj j
⊢ Nonempty (StructuredArrow d F)
C : Type v
inst✝² : Category C
D : Type v
inst✝¹ : Category D
F : C ⥤ D
inst✝ : Final F
I : (d : D) → colimit (F ⋙ coyoneda.obj d.op) ≅ PUnit
d : D
this : colimit (F ⋙ coyoneda.obj d.op)
⊢ Nonempty (StructuredArrow d F)
obtain ⟨j, y, rfl⟩ := Limits.Types.jointly_surjective'.{v, v} this
no goals
case intro.intro
C : Type v
inst✝² : Category C
D : Type v
inst✝¹ : Category D
F : C ⥤ D
inst✝ : Final F
I : (d : D) → colimit (F ⋙ coyoneda.obj d.op) ≅ PUnit
d : D
j : C
y : (F ⋙ coyoneda.obj d.op).obj j
⊢ Nonempty (StructuredArrow d F)
exact ⟨StructuredArrow.mk y⟩
case a
C : Type v
inst✝² : Category C
D : Type v
inst✝¹ : Category D
F : C ⥤ D
inst✝ : Final F
I : (d : D) → colimit (F ⋙ coyoneda.obj d.op) ≅ PUnit
d : D
this : Nonempty (StructuredArrow d F)
X₁ : C
f₁ : (fromPUnit d).obj { as := PUnit.unit } ⟶ F.obj X₁
X₂ : C
f₂ : (fromPUnit d).obj { as := PUnit.unit } ⟶ F.obj X₂
y₁ : colimit (F ⋙ coyoneda.obj d.op) := colimit.ι (F ⋙ coyoneda.obj d.op) X₁ f₁
y₂ : colimit (F ⋙ coyoneda.obj d.op) := colimit.ι (F ⋙ coyoneda.obj d.op) X₂ f₂
⊢ ↑(I d).toEquiv y₁ = ↑(I d).toEquiv y₂
C : Type v
inst✝² : Category C
D : Type v
inst✝¹ : Category D
F : C ⥤ D
inst✝ : Final F
I : (d : D) → colimit (F ⋙ coyoneda.obj d.op) ≅ PUnit
d : D
this : Nonempty (StructuredArrow d F)
X₁ : C
f₁ : (fromPUnit d).obj { as := PUnit.unit } ⟶ F.obj X₁
X₂ : C
f₂ : (fromPUnit d).obj { as := PUnit.unit } ⟶ F.obj X₂
y₁ : colimit (F ⋙ coyoneda.obj d.op) := colimit.ι (F ⋙ coyoneda.obj d.op) X₁ f₁
y₂ : colimit (F ⋙ coyoneda.obj d.op) := colimit.ι (F ⋙ coyoneda.obj d.op) X₂ f₂
⊢ y₁ = y₂
apply (I d).toEquiv.injective
no goals
case a
C : Type v
inst✝² : Category C
D : Type v
inst✝¹ : Category D
F : C ⥤ D
inst✝ : Final F
I : (d : D) → colimit (F ⋙ coyoneda.obj d.op) ≅ PUnit
d : D
this : Nonempty (StructuredArrow d F)
X₁ : C
f₁ : (fromPUnit d).obj { as := PUnit.unit } ⟶ F.obj X₁
X₂ : C
f₂ : (fromPUnit d).obj { as := PUnit.unit } ⟶ F.obj X₂
y₁ : colimit (F ⋙ coyoneda.obj d.op) := colimit.ι (F ⋙ coyoneda.obj d.op) X₁ f₁
y₂ : colimit (F ⋙ coyoneda.obj d.op) := colimit.ι (F ⋙ coyoneda.obj d.op) X₂ f₂
⊢ ↑(I d).toEquiv y₁ = ↑(I d).toEquiv y₂
ext