J : Type v'
inst✝² : Category J
C : Type u
inst✝¹ : Category C
X Y : C
inst✝ : HasInitial C
H : IsUniversalColimit (BinaryCofan.mk (𝟙 (⊥_ C)) (𝟙 (⊥_ C)))
A : C
f : A ⟶ ⊥_ C
⊢ IsIso f
J : Type v'
inst✝² : Category J
C : Type u
inst✝¹ : Category C
X Y : C
inst✝ : HasInitial C
H : IsUniversalColimit (BinaryCofan.mk (𝟙 (⊥_ C)) (𝟙 (⊥_ C)))
⊢ ∀ (A : C) (f : A ⟶ ⊥_ C), IsIso f
intro A f
J : Type v'
inst✝² : Category J
C : Type u
inst✝¹ : Category C
X Y : C
inst✝ : HasInitial C
H : IsUniversalColimit (BinaryCofan.mk (𝟙 (⊥_ C)) (𝟙 (⊥_ C)))
A : C
f : A ⟶ ⊥_ C
⊢ IsColimit (BinaryCofan.mk (𝟙 A) (𝟙 A))
J : Type v'
inst✝² : Category J
C : Type u
inst✝¹ : Category C
X Y : C
inst✝ : HasInitial C
H : IsUniversalColimit (BinaryCofan.mk (𝟙 (⊥_ C)) (𝟙 (⊥_ C)))
A : C
f : A ⟶ ⊥_ C
⊢ IsIso f
suffices IsColimit (BinaryCofan.mk (𝟙 A) (𝟙 A)) by
  obtain ⟨l, h₁, h₂⟩ := Limits.BinaryCofan.IsColimit.desc' this (f ≫ initial.to A) (𝟙 A)
  rcases(Category.id_comp _).symm.trans h₂ with rfl
  exact ⟨⟨_, ((Category.id_comp _).symm.trans h₁).symm, initialIsInitial.hom_ext _ _⟩⟩
J : Type v'
inst✝² : Category J
C : Type u
inst✝¹ : Category C
X Y : C
inst✝ : HasInitial C
H : IsUniversalColimit (BinaryCofan.mk (𝟙 (⊥_ C)) (𝟙 (⊥_ C)))
A : C
f : A ⟶ ⊥_ C
⊢ ∀ (j : Discrete WalkingPair),
    IsPullback ((BinaryCofan.mk (𝟙 A) (𝟙 A)).ι.app j) ((mapPair f f).app j) f
      ((BinaryCofan.mk (𝟙 (⊥_ C)) (𝟙 (⊥_ C))).ι.app j)
J : Type v'
inst✝² : Category J
C : Type u
inst✝¹ : Category C
X Y : C
inst✝ : HasInitial C
H : IsUniversalColimit (BinaryCofan.mk (𝟙 (⊥_ C)) (𝟙 (⊥_ C)))
A : C
f : A ⟶ ⊥_ C
⊢ IsColimit (BinaryCofan.mk (𝟙 A) (𝟙 A))
refine' (H (BinaryCofan.mk (𝟙 _) (𝟙 _)) (mapPair f f) f (by ext ⟨⟨⟩⟩ <;> dsimp <;> simp)
  (mapPair_equifibered _) _).some
no goals
J : Type v'
inst✝² : Category J
C : Type u
inst✝¹ : Category C
X Y : C
inst✝ : HasInitial C
H : IsUniversalColimit (BinaryCofan.mk (𝟙 (⊥_ C)) (𝟙 (⊥_ C)))
A : C
f : A ⟶ ⊥_ C
⊢ ∀ (j : Discrete WalkingPair),
    IsPullback ((BinaryCofan.mk (𝟙 A) (𝟙 A)).ι.app j) ((mapPair f f).app j) f
      ((BinaryCofan.mk (𝟙 (⊥_ C)) (𝟙 (⊥_ C))).ι.app j)
rintro ⟨⟨⟩⟩ <;> dsimp <;>
  exact IsPullback.of_horiz_isIso ⟨(Category.id_comp _).trans (Category.comp_id _).symm⟩
case mk.intro
J : Type v'
inst✝² : Category J
C : Type u
inst✝¹ : Category C
X Y : C
inst✝ : HasInitial C
H : IsUniversalColimit (BinaryCofan.mk (𝟙 (⊥_ C)) (𝟙 (⊥_ C)))
A : C
f : A ⟶ ⊥_ C
this : IsColimit (BinaryCofan.mk (𝟙 A) (𝟙 A))
l : (BinaryCofan.mk (𝟙 A) (𝟙 A)).pt ⟶ A
h₁ : BinaryCofan.inl (BinaryCofan.mk (𝟙 A) (𝟙 A)) ≫ l = f ≫ initial.to A
h₂ : BinaryCofan.inr (BinaryCofan.mk (𝟙 A) (𝟙 A)) ≫ l = 𝟙 A
⊢ IsIso f
J : Type v'
inst✝² : Category J
C : Type u
inst✝¹ : Category C
X Y : C
inst✝ : HasInitial C
H : IsUniversalColimit (BinaryCofan.mk (𝟙 (⊥_ C)) (𝟙 (⊥_ C)))
A : C
f : A ⟶ ⊥_ C
this : IsColimit (BinaryCofan.mk (𝟙 A) (𝟙 A))
⊢ IsIso f
obtain ⟨l, h₁, h₂⟩ := Limits.BinaryCofan.IsColimit.desc' this (f ≫ initial.to A) (𝟙 A)
case mk.intro
J : Type v'
inst✝² : Category J
C : Type u
inst✝¹ : Category C
X Y : C
inst✝ : HasInitial C
H : IsUniversalColimit (BinaryCofan.mk (𝟙 (⊥_ C)) (𝟙 (⊥_ C)))
A : C
f : A ⟶ ⊥_ C
this : IsColimit (BinaryCofan.mk (𝟙 A) (𝟙 A))
h₁ : BinaryCofan.inl (BinaryCofan.mk (𝟙 A) (𝟙 A)) ≫ 𝟙 A = f ≫ initial.to A
h₂ : BinaryCofan.inr (BinaryCofan.mk (𝟙 A) (𝟙 A)) ≫ 𝟙 A = 𝟙 A
⊢ IsIso f
case mk.intro
J : Type v'
inst✝² : Category J
C : Type u
inst✝¹ : Category C
X Y : C
inst✝ : HasInitial C
H : IsUniversalColimit (BinaryCofan.mk (𝟙 (⊥_ C)) (𝟙 (⊥_ C)))
A : C
f : A ⟶ ⊥_ C
this : IsColimit (BinaryCofan.mk (𝟙 A) (𝟙 A))
l : (BinaryCofan.mk (𝟙 A) (𝟙 A)).pt ⟶ A
h₁ : BinaryCofan.inl (BinaryCofan.mk (𝟙 A) (𝟙 A)) ≫ l = f ≫ initial.to A
h₂ : BinaryCofan.inr (BinaryCofan.mk (𝟙 A) (𝟙 A)) ≫ l = 𝟙 A
⊢ IsIso f
rcases(Category.id_comp _).symm.trans h₂ with rfl
no goals
case mk.intro
J : Type v'
inst✝² : Category J
C : Type u
inst✝¹ : Category C
X Y : C
inst✝ : HasInitial C
H : IsUniversalColimit (BinaryCofan.mk (𝟙 (⊥_ C)) (𝟙 (⊥_ C)))
A : C
f : A ⟶ ⊥_ C
this : IsColimit (BinaryCofan.mk (𝟙 A) (𝟙 A))
h₁ : BinaryCofan.inl (BinaryCofan.mk (𝟙 A) (𝟙 A)) ≫ 𝟙 A = f ≫ initial.to A
h₂ : BinaryCofan.inr (BinaryCofan.mk (𝟙 A) (𝟙 A)) ≫ 𝟙 A = 𝟙 A
⊢ IsIso f
exact ⟨⟨_, ((Category.id_comp _).symm.trans h₁).symm, initialIsInitial.hom_ext _ _⟩⟩
no goals
J : Type v'
inst✝² : Category J
C : Type u
inst✝¹ : Category C
X Y : C
inst✝ : HasInitial C
H : IsUniversalColimit (BinaryCofan.mk (𝟙 (⊥_ C)) (𝟙 (⊥_ C)))
A : C
f : A ⟶ ⊥_ C
⊢ mapPair f f ≫ (BinaryCofan.mk (𝟙 (⊥_ C)) (𝟙 (⊥_ C))).ι =
    (BinaryCofan.mk (𝟙 A) (𝟙 A)).ι ≫ (Functor.const (Discrete WalkingPair)).map f
ext ⟨⟨⟩⟩ <;> dsimp <;> simp