case mp
C : Type u
inst✝ : Category C
X✝ Y✝ X Y : C
h : IsInitial Y
c : BinaryCofan X Y
⊢ Nonempty (IsColimit c) → IsIso (inl c)

case mpr
C : Type u
inst✝ : Category C
X✝ Y✝ X Y : C
h : IsInitial Y
c : BinaryCofan X Y
⊢ IsIso (inl c) → Nonempty (IsColimit c)
C : Type u
inst✝ : Category C
X✝ Y✝ X Y : C
h : IsInitial Y
c : BinaryCofan X Y
⊢ Nonempty (IsColimit c) ↔ IsIso (inl c)
constructor
case mp.intro
C : Type u
inst✝ : Category C
X✝ Y✝ X Y : C
h : IsInitial Y
c : BinaryCofan X Y
H : IsColimit c
⊢ IsIso (inl c)
case mp
C : Type u
inst✝ : Category C
X✝ Y✝ X Y : C
h : IsInitial Y
c : BinaryCofan X Y
⊢ Nonempty (IsColimit c) → IsIso (inl c)
rintro ⟨H⟩
case mp.intro.mk.intro
C : Type u
inst✝ : Category C
X✝ Y✝ X Y : C
h : IsInitial Y
c : BinaryCofan X Y
H : IsColimit c
l : c.pt ⟶ X
hl : inl c ≫ l = 𝟙 X
⊢ IsIso (inl c)
case mp.intro
C : Type u
inst✝ : Category C
X✝ Y✝ X Y : C
h : IsInitial Y
c : BinaryCofan X Y
H : IsColimit c
⊢ IsIso (inl c)
obtain ⟨l, hl, -⟩ := BinaryCofan.IsColimit.desc' H (𝟙 X) (h.to X)
case mp.intro.mk.intro
C : Type u
inst✝ : Category C
X✝ Y✝ X Y : C
h : IsInitial Y
c : BinaryCofan X Y
H : IsColimit c
l : c.pt ⟶ X
hl : inl c ≫ l = 𝟙 X
⊢ inl c ≫ l ≫ inl c = inl c ≫ 𝟙 (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := left })
case mp.intro.mk.intro
C : Type u
inst✝ : Category C
X✝ Y✝ X Y : C
h : IsInitial Y
c : BinaryCofan X Y
H : IsColimit c
l : c.pt ⟶ X
hl : inl c ≫ l = 𝟙 X
⊢ IsIso (inl c)
refine ⟨⟨l, hl, BinaryCofan.IsColimit.hom_ext H (?_) (h.hom_ext _ _)⟩⟩
case mp.intro.mk.intro
C : Type u
inst✝ : Category C
X✝ Y✝ X Y : C
h : IsInitial Y
c : BinaryCofan X Y
H : IsColimit c
l : c.pt ⟶ X
hl : inl c ≫ l = 𝟙 X
⊢ inl c ≫ l ≫ inl c = inl c
case mp.intro.mk.intro
C : Type u
inst✝ : Category C
X✝ Y✝ X Y : C
h : IsInitial Y
c : BinaryCofan X Y
H : IsColimit c
l : c.pt ⟶ X
hl : inl c ≫ l = 𝟙 X
⊢ inl c ≫ l ≫ inl c = inl c ≫ 𝟙 (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := left })
rw [Category.comp_id]
no goals
case mp.intro.mk.intro
C : Type u
inst✝ : Category C
X✝ Y✝ X Y : C
h : IsInitial Y
c : BinaryCofan X Y
H : IsColimit c
l : c.pt ⟶ X
hl : inl c ≫ l = 𝟙 X
e : (inl c ≫ l) ≫ inl c = 𝟙 X ≫ inl c
⊢ inl c ≫ l ≫ inl c = inl c
rwa [Category.assoc,Category.id_comp] at e
case mpr
C : Type u
inst✝ : Category C
X✝ Y✝ X Y : C
h : IsInitial Y
c : BinaryCofan X Y
a✝ : IsIso (inl c)
⊢ Nonempty (IsColimit c)
case mpr
C : Type u
inst✝ : Category C
X✝ Y✝ X Y : C
h : IsInitial Y
c : BinaryCofan X Y
⊢ IsIso (inl c) → Nonempty (IsColimit c)
intro
no goals
case mpr
C : Type u
inst✝ : Category C
X✝ Y✝ X Y : C
h : IsInitial Y
c : BinaryCofan X Y
a✝ : IsIso (inl c)
⊢ Nonempty (IsColimit c)
exact
  ⟨BinaryCofan.IsColimit.mk _ (fun f _ => inv c.inl ≫ f)
      (fun _ _ => IsIso.hom_inv_id_assoc _ _) (fun _ _ => h.hom_ext _ _) fun _ _ _ e _ =>
      (IsIso.eq_inv_comp _).mpr e⟩