C : Type u
inst✝ : Category C
X✝ Y✝ X Y : C
h : IsInitial X
c : BinaryCofan X Y
⊢ Nonempty (IsColimit c) ↔ Nonempty (IsColimit (mk (inr c) (inl c)))
C : Type u
inst✝ : Category C
X✝ Y✝ X Y : C
h : IsInitial X
c : BinaryCofan X Y
⊢ Nonempty (IsColimit c) ↔ IsIso (inr c)
refine' Iff.trans _ (BinaryCofan.isColimit_iff_isIso_inl h (BinaryCofan.mk c.inr c.inl))
no goals
C : Type u
inst✝ : Category C
X✝ Y✝ X Y : C
h : IsInitial X
c : BinaryCofan X Y
⊢ Nonempty (IsColimit c) ↔ Nonempty (IsColimit (mk (inr c) (inl c)))
exact
  ⟨fun h => ⟨BinaryCofan.isColimitFlip h.some⟩, fun h =>
    ⟨(BinaryCofan.isColimitFlip h.some).ofIsoColimit (isoBinaryCofanMk c).symm⟩⟩