J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
X✝ Y✝ X Y : C
c : BinaryCofan X Y
cofans : (X Y : C) → BinaryCofan X Y
colimits : (X Y : C) → IsColimit (cofans X Y)
cones : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → PullbackCone f g
limits : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → IsLimit (cones f g)
h₁ :
  ∀ {X' Y' : C} (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : (cofans X' Y').pt ⟶ c.pt),
    αX ≫ BinaryCofan.inl c = BinaryCofan.inl (cofans X' Y') ≫ f →
      αY ≫ BinaryCofan.inr c = BinaryCofan.inr (cofans X' Y') ≫ f →
        IsPullback (BinaryCofan.inl (cofans X' Y')) αX f (BinaryCofan.inl c) ∧
          IsPullback (BinaryCofan.inr (cofans X' Y')) αY f (BinaryCofan.inr c)
h₂ :
  {Z : C} →
    (f : Z ⟶ c.pt) →
      IsColimit
        (BinaryCofan.mk (PullbackCone.fst (cones f (BinaryCofan.inl c)))
          (PullbackCone.fst (cones f (BinaryCofan.inr c))))
⊢ ∀ {X' Y' : C} (c' : BinaryCofan X' Y') (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : c'.pt ⟶ c.pt),
    αX ≫ BinaryCofan.inl c = BinaryCofan.inl c' ≫ f →
      αY ≫ BinaryCofan.inr c = BinaryCofan.inr c' ≫ f →
        (Nonempty (IsColimit c') ↔
          IsPullback (BinaryCofan.inl c') αX f (BinaryCofan.inl c) ∧
            IsPullback (BinaryCofan.inr c') αY f (BinaryCofan.inr c))
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
X✝ Y✝ X Y : C
c : BinaryCofan X Y
cofans : (X Y : C) → BinaryCofan X Y
colimits : (X Y : C) → IsColimit (cofans X Y)
cones : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → PullbackCone f g
limits : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → IsLimit (cones f g)
h₁ :
  ∀ {X' Y' : C} (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : (cofans X' Y').pt ⟶ c.pt),
    αX ≫ BinaryCofan.inl c = BinaryCofan.inl (cofans X' Y') ≫ f →
      αY ≫ BinaryCofan.inr c = BinaryCofan.inr (cofans X' Y') ≫ f →
        IsPullback (BinaryCofan.inl (cofans X' Y')) αX f (BinaryCofan.inl c) ∧
          IsPullback (BinaryCofan.inr (cofans X' Y')) αY f (BinaryCofan.inr c)
h₂ :
  {Z : C} →
    (f : Z ⟶ c.pt) →
      IsColimit
        (BinaryCofan.mk (PullbackCone.fst (cones f (BinaryCofan.inl c)))
          (PullbackCone.fst (cones f (BinaryCofan.inr c))))
⊢ IsVanKampenColimit c
rw [BinaryCofan.isVanKampen_iff]
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
X✝ Y✝ X Y : C
c : BinaryCofan X Y
cofans : (X Y : C) → BinaryCofan X Y
colimits : (X Y : C) → IsColimit (cofans X Y)
cones : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → PullbackCone f g
limits : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → IsLimit (cones f g)
h₁ :
  ∀ {X' Y' : C} (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : (cofans X' Y').pt ⟶ c.pt),
    αX ≫ BinaryCofan.inl c = BinaryCofan.inl (cofans X' Y') ≫ f →
      αY ≫ BinaryCofan.inr c = BinaryCofan.inr (cofans X' Y') ≫ f →
        IsPullback (BinaryCofan.inl (cofans X' Y')) αX f (BinaryCofan.inl c) ∧
          IsPullback (BinaryCofan.inr (cofans X' Y')) αY f (BinaryCofan.inr c)
h₂ :
  {Z : C} →
    (f : Z ⟶ c.pt) →
      IsColimit
        (BinaryCofan.mk (PullbackCone.fst (cones f (BinaryCofan.inl c)))
          (PullbackCone.fst (cones f (BinaryCofan.inr c))))
X' Y' : C
c' : BinaryCofan X' Y'
αX : X' ⟶ X
αY : Y' ⟶ Y
f : c'.pt ⟶ c.pt
hX : αX ≫ BinaryCofan.inl c = BinaryCofan.inl c' ≫ f
hY : αY ≫ BinaryCofan.inr c = BinaryCofan.inr c' ≫ f
⊢ Nonempty (IsColimit c') ↔
    IsPullback (BinaryCofan.inl c') αX f (BinaryCofan.inl c) ∧ IsPullback (BinaryCofan.inr c') αY f (BinaryCofan.inr c)
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
X✝ Y✝ X Y : C
c : BinaryCofan X Y
cofans : (X Y : C) → BinaryCofan X Y
colimits : (X Y : C) → IsColimit (cofans X Y)
cones : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → PullbackCone f g
limits : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → IsLimit (cones f g)
h₁ :
  ∀ {X' Y' : C} (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : (cofans X' Y').pt ⟶ c.pt),
    αX ≫ BinaryCofan.inl c = BinaryCofan.inl (cofans X' Y') ≫ f →
      αY ≫ BinaryCofan.inr c = BinaryCofan.inr (cofans X' Y') ≫ f →
        IsPullback (BinaryCofan.inl (cofans X' Y')) αX f (BinaryCofan.inl c) ∧
          IsPullback (BinaryCofan.inr (cofans X' Y')) αY f (BinaryCofan.inr c)
h₂ :
  {Z : C} →
    (f : Z ⟶ c.pt) →
      IsColimit
        (BinaryCofan.mk (PullbackCone.fst (cones f (BinaryCofan.inl c)))
          (PullbackCone.fst (cones f (BinaryCofan.inr c))))
⊢ ∀ {X' Y' : C} (c' : BinaryCofan X' Y') (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : c'.pt ⟶ c.pt),
    αX ≫ BinaryCofan.inl c = BinaryCofan.inl c' ≫ f →
      αY ≫ BinaryCofan.inr c = BinaryCofan.inr c' ≫ f →
        (Nonempty (IsColimit c') ↔
          IsPullback (BinaryCofan.inl c') αX f (BinaryCofan.inl c) ∧
            IsPullback (BinaryCofan.inr c') αY f (BinaryCofan.inr c))
introv hX hY
case mp
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
X✝ Y✝ X Y : C
c : BinaryCofan X Y
cofans : (X Y : C) → BinaryCofan X Y
colimits : (X Y : C) → IsColimit (cofans X Y)
cones : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → PullbackCone f g
limits : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → IsLimit (cones f g)
h₁ :
  ∀ {X' Y' : C} (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : (cofans X' Y').pt ⟶ c.pt),
    αX ≫ BinaryCofan.inl c = BinaryCofan.inl (cofans X' Y') ≫ f →
      αY ≫ BinaryCofan.inr c = BinaryCofan.inr (cofans X' Y') ≫ f →
        IsPullback (BinaryCofan.inl (cofans X' Y')) αX f (BinaryCofan.inl c) ∧
          IsPullback (BinaryCofan.inr (cofans X' Y')) αY f (BinaryCofan.inr c)
h₂ :
  {Z : C} →
    (f : Z ⟶ c.pt) →
      IsColimit
        (BinaryCofan.mk (PullbackCone.fst (cones f (BinaryCofan.inl c)))
          (PullbackCone.fst (cones f (BinaryCofan.inr c))))
X' Y' : C
c' : BinaryCofan X' Y'
αX : X' ⟶ X
αY : Y' ⟶ Y
f : c'.pt ⟶ c.pt
hX : αX ≫ BinaryCofan.inl c = BinaryCofan.inl c' ≫ f
hY : αY ≫ BinaryCofan.inr c = BinaryCofan.inr c' ≫ f
⊢ Nonempty (IsColimit c') →
    IsPullback (BinaryCofan.inl c') αX f (BinaryCofan.inl c) ∧ IsPullback (BinaryCofan.inr c') αY f (BinaryCofan.inr c)

case mpr
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
X✝ Y✝ X Y : C
c : BinaryCofan X Y
cofans : (X Y : C) → BinaryCofan X Y
colimits : (X Y : C) → IsColimit (cofans X Y)
cones : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → PullbackCone f g
limits : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → IsLimit (cones f g)
h₁ :
  ∀ {X' Y' : C} (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : (cofans X' Y').pt ⟶ c.pt),
    αX ≫ BinaryCofan.inl c = BinaryCofan.inl (cofans X' Y') ≫ f →
      αY ≫ BinaryCofan.inr c = BinaryCofan.inr (cofans X' Y') ≫ f →
        IsPullback (BinaryCofan.inl (cofans X' Y')) αX f (BinaryCofan.inl c) ∧
          IsPullback (BinaryCofan.inr (cofans X' Y')) αY f (BinaryCofan.inr c)
h₂ :
  {Z : C} →
    (f : Z ⟶ c.pt) →
      IsColimit
        (BinaryCofan.mk (PullbackCone.fst (cones f (BinaryCofan.inl c)))
          (PullbackCone.fst (cones f (BinaryCofan.inr c))))
X' Y' : C
c' : BinaryCofan X' Y'
αX : X' ⟶ X
αY : Y' ⟶ Y
f : c'.pt ⟶ c.pt
hX : αX ≫ BinaryCofan.inl c = BinaryCofan.inl c' ≫ f
hY : αY ≫ BinaryCofan.inr c = BinaryCofan.inr c' ≫ f
⊢ IsPullback (BinaryCofan.inl c') αX f (BinaryCofan.inl c) ∧ IsPullback (BinaryCofan.inr c') αY f (BinaryCofan.inr c) →
    Nonempty (IsColimit c')
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
X✝ Y✝ X Y : C
c : BinaryCofan X Y
cofans : (X Y : C) → BinaryCofan X Y
colimits : (X Y : C) → IsColimit (cofans X Y)
cones : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → PullbackCone f g
limits : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → IsLimit (cones f g)
h₁ :
  ∀ {X' Y' : C} (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : (cofans X' Y').pt ⟶ c.pt),
    αX ≫ BinaryCofan.inl c = BinaryCofan.inl (cofans X' Y') ≫ f →
      αY ≫ BinaryCofan.inr c = BinaryCofan.inr (cofans X' Y') ≫ f →
        IsPullback (BinaryCofan.inl (cofans X' Y')) αX f (BinaryCofan.inl c) ∧
          IsPullback (BinaryCofan.inr (cofans X' Y')) αY f (BinaryCofan.inr c)
h₂ :
  {Z : C} →
    (f : Z ⟶ c.pt) →
      IsColimit
        (BinaryCofan.mk (PullbackCone.fst (cones f (BinaryCofan.inl c)))
          (PullbackCone.fst (cones f (BinaryCofan.inr c))))
X' Y' : C
c' : BinaryCofan X' Y'
αX : X' ⟶ X
αY : Y' ⟶ Y
f : c'.pt ⟶ c.pt
hX : αX ≫ BinaryCofan.inl c = BinaryCofan.inl c' ≫ f
hY : αY ≫ BinaryCofan.inr c = BinaryCofan.inr c' ≫ f
⊢ Nonempty (IsColimit c') ↔
    IsPullback (BinaryCofan.inl c') αX f (BinaryCofan.inl c) ∧ IsPullback (BinaryCofan.inr c') αY f (BinaryCofan.inr c)
constructor
case mp.intro
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
X✝ Y✝ X Y : C
c : BinaryCofan X Y
cofans : (X Y : C) → BinaryCofan X Y
colimits : (X Y : C) → IsColimit (cofans X Y)
cones : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → PullbackCone f g
limits : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → IsLimit (cones f g)
h₁ :
  ∀ {X' Y' : C} (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : (cofans X' Y').pt ⟶ c.pt),
    αX ≫ BinaryCofan.inl c = BinaryCofan.inl (cofans X' Y') ≫ f →
      αY ≫ BinaryCofan.inr c = BinaryCofan.inr (cofans X' Y') ≫ f →
        IsPullback (BinaryCofan.inl (cofans X' Y')) αX f (BinaryCofan.inl c) ∧
          IsPullback (BinaryCofan.inr (cofans X' Y')) αY f (BinaryCofan.inr c)
h₂ :
  {Z : C} →
    (f : Z ⟶ c.pt) →
      IsColimit
        (BinaryCofan.mk (PullbackCone.fst (cones f (BinaryCofan.inl c)))
          (PullbackCone.fst (cones f (BinaryCofan.inr c))))
X' Y' : C
c' : BinaryCofan X' Y'
αX : X' ⟶ X
αY : Y' ⟶ Y
f : c'.pt ⟶ c.pt
hX : αX ≫ BinaryCofan.inl c = BinaryCofan.inl c' ≫ f
hY : αY ≫ BinaryCofan.inr c = BinaryCofan.inr c' ≫ f
h : IsColimit c'
⊢ IsPullback (BinaryCofan.inl c') αX f (BinaryCofan.inl c) ∧ IsPullback (BinaryCofan.inr c') αY f (BinaryCofan.inr c)
case mp
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
X✝ Y✝ X Y : C
c : BinaryCofan X Y
cofans : (X Y : C) → BinaryCofan X Y
colimits : (X Y : C) → IsColimit (cofans X Y)
cones : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → PullbackCone f g
limits : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → IsLimit (cones f g)
h₁ :
  ∀ {X' Y' : C} (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : (cofans X' Y').pt ⟶ c.pt),
    αX ≫ BinaryCofan.inl c = BinaryCofan.inl (cofans X' Y') ≫ f →
      αY ≫ BinaryCofan.inr c = BinaryCofan.inr (cofans X' Y') ≫ f →
        IsPullback (BinaryCofan.inl (cofans X' Y')) αX f (BinaryCofan.inl c) ∧
          IsPullback (BinaryCofan.inr (cofans X' Y')) αY f (BinaryCofan.inr c)
h₂ :
  {Z : C} →
    (f : Z ⟶ c.pt) →
      IsColimit
        (BinaryCofan.mk (PullbackCone.fst (cones f (BinaryCofan.inl c)))
          (PullbackCone.fst (cones f (BinaryCofan.inr c))))
X' Y' : C
c' : BinaryCofan X' Y'
αX : X' ⟶ X
αY : Y' ⟶ Y
f : c'.pt ⟶ c.pt
hX : αX ≫ BinaryCofan.inl c = BinaryCofan.inl c' ≫ f
hY : αY ≫ BinaryCofan.inr c = BinaryCofan.inr c' ≫ f
⊢ Nonempty (IsColimit c') →
    IsPullback (BinaryCofan.inl c') αX f (BinaryCofan.inl c) ∧ IsPullback (BinaryCofan.inr c') αY f (BinaryCofan.inr c)
rintro ⟨h⟩
case mp.intro
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
X✝ Y✝ X Y : C
c : BinaryCofan X Y
cofans : (X Y : C) → BinaryCofan X Y
colimits : (X Y : C) → IsColimit (cofans X Y)
cones : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → PullbackCone f g
limits : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → IsLimit (cones f g)
h₁ :
  ∀ {X' Y' : C} (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : (cofans X' Y').pt ⟶ c.pt),
    αX ≫ BinaryCofan.inl c = BinaryCofan.inl (cofans X' Y') ≫ f →
      αY ≫ BinaryCofan.inr c = BinaryCofan.inr (cofans X' Y') ≫ f →
        IsPullback (BinaryCofan.inl (cofans X' Y')) αX f (BinaryCofan.inl c) ∧
          IsPullback (BinaryCofan.inr (cofans X' Y')) αY f (BinaryCofan.inr c)
h₂ :
  {Z : C} →
    (f : Z ⟶ c.pt) →
      IsColimit
        (BinaryCofan.mk (PullbackCone.fst (cones f (BinaryCofan.inl c)))
          (PullbackCone.fst (cones f (BinaryCofan.inr c))))
X' Y' : C
c' : BinaryCofan X' Y'
αX : X' ⟶ X
αY : Y' ⟶ Y
f : c'.pt ⟶ c.pt
hX : αX ≫ BinaryCofan.inl c = BinaryCofan.inl c' ≫ f
hY : αY ≫ BinaryCofan.inr c = BinaryCofan.inr c' ≫ f
h : IsColimit c'
e : c'.pt ≅ (cofans X' Y').pt := IsColimit.coconePointUniqueUpToIso h (colimits X' Y')
⊢ IsPullback (BinaryCofan.inl c') αX f (BinaryCofan.inl c) ∧ IsPullback (BinaryCofan.inr c') αY f (BinaryCofan.inr c)
case mp.intro
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
X✝ Y✝ X Y : C
c : BinaryCofan X Y
cofans : (X Y : C) → BinaryCofan X Y
colimits : (X Y : C) → IsColimit (cofans X Y)
cones : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → PullbackCone f g
limits : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → IsLimit (cones f g)
h₁ :
  ∀ {X' Y' : C} (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : (cofans X' Y').pt ⟶ c.pt),
    αX ≫ BinaryCofan.inl c = BinaryCofan.inl (cofans X' Y') ≫ f →
      αY ≫ BinaryCofan.inr c = BinaryCofan.inr (cofans X' Y') ≫ f →
        IsPullback (BinaryCofan.inl (cofans X' Y')) αX f (BinaryCofan.inl c) ∧
          IsPullback (BinaryCofan.inr (cofans X' Y')) αY f (BinaryCofan.inr c)
h₂ :
  {Z : C} →
    (f : Z ⟶ c.pt) →
      IsColimit
        (BinaryCofan.mk (PullbackCone.fst (cones f (BinaryCofan.inl c)))
          (PullbackCone.fst (cones f (BinaryCofan.inr c))))
X' Y' : C
c' : BinaryCofan X' Y'
αX : X' ⟶ X
αY : Y' ⟶ Y
f : c'.pt ⟶ c.pt
hX : αX ≫ BinaryCofan.inl c = BinaryCofan.inl c' ≫ f
hY : αY ≫ BinaryCofan.inr c = BinaryCofan.inr c' ≫ f
h : IsColimit c'
⊢ IsPullback (BinaryCofan.inl c') αX f (BinaryCofan.inl c) ∧ IsPullback (BinaryCofan.inr c') αY f (BinaryCofan.inr c)
let e := h.coconePointUniqueUpToIso (colimits _ _)
case mp.intro.intro
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
X✝ Y✝ X Y : C
c : BinaryCofan X Y
cofans : (X Y : C) → BinaryCofan X Y
colimits : (X Y : C) → IsColimit (cofans X Y)
cones : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → PullbackCone f g
limits : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → IsLimit (cones f g)
h₁ :
  ∀ {X' Y' : C} (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : (cofans X' Y').pt ⟶ c.pt),
    αX ≫ BinaryCofan.inl c = BinaryCofan.inl (cofans X' Y') ≫ f →
      αY ≫ BinaryCofan.inr c = BinaryCofan.inr (cofans X' Y') ≫ f →
        IsPullback (BinaryCofan.inl (cofans X' Y')) αX f (BinaryCofan.inl c) ∧
          IsPullback (BinaryCofan.inr (cofans X' Y')) αY f (BinaryCofan.inr c)
h₂ :
  {Z : C} →
    (f : Z ⟶ c.pt) →
      IsColimit
        (BinaryCofan.mk (PullbackCone.fst (cones f (BinaryCofan.inl c)))
          (PullbackCone.fst (cones f (BinaryCofan.inr c))))
X' Y' : C
c' : BinaryCofan X' Y'
αX : X' ⟶ X
αY : Y' ⟶ Y
f : c'.pt ⟶ c.pt
hX : αX ≫ BinaryCofan.inl c = BinaryCofan.inl c' ≫ f
hY : αY ≫ BinaryCofan.inr c = BinaryCofan.inr c' ≫ f
h : IsColimit c'
e : c'.pt ≅ (cofans X' Y').pt := IsColimit.coconePointUniqueUpToIso h (colimits X' Y')
hl : IsPullback (BinaryCofan.inl (cofans X' Y')) αX (e.inv ≫ f) (BinaryCofan.inl c)
hr : IsPullback (BinaryCofan.inr (cofans X' Y')) αY (e.inv ≫ f) (BinaryCofan.inr c)
⊢ IsPullback (BinaryCofan.inl c') αX f (BinaryCofan.inl c) ∧ IsPullback (BinaryCofan.inr c') αY f (BinaryCofan.inr c)
case mp.intro
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
X✝ Y✝ X Y : C
c : BinaryCofan X Y
cofans : (X Y : C) → BinaryCofan X Y
colimits : (X Y : C) → IsColimit (cofans X Y)
cones : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → PullbackCone f g
limits : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → IsLimit (cones f g)
h₁ :
  ∀ {X' Y' : C} (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : (cofans X' Y').pt ⟶ c.pt),
    αX ≫ BinaryCofan.inl c = BinaryCofan.inl (cofans X' Y') ≫ f →
      αY ≫ BinaryCofan.inr c = BinaryCofan.inr (cofans X' Y') ≫ f →
        IsPullback (BinaryCofan.inl (cofans X' Y')) αX f (BinaryCofan.inl c) ∧
          IsPullback (BinaryCofan.inr (cofans X' Y')) αY f (BinaryCofan.inr c)
h₂ :
  {Z : C} →
    (f : Z ⟶ c.pt) →
      IsColimit
        (BinaryCofan.mk (PullbackCone.fst (cones f (BinaryCofan.inl c)))
          (PullbackCone.fst (cones f (BinaryCofan.inr c))))
X' Y' : C
c' : BinaryCofan X' Y'
αX : X' ⟶ X
αY : Y' ⟶ Y
f : c'.pt ⟶ c.pt
hX : αX ≫ BinaryCofan.inl c = BinaryCofan.inl c' ≫ f
hY : αY ≫ BinaryCofan.inr c = BinaryCofan.inr c' ≫ f
h : IsColimit c'
e : c'.pt ≅ (cofans X' Y').pt := IsColimit.coconePointUniqueUpToIso h (colimits X' Y')
⊢ IsPullback (BinaryCofan.inl c') αX f (BinaryCofan.inl c) ∧ IsPullback (BinaryCofan.inr c') αY f (BinaryCofan.inr c)
obtain ⟨hl, hr⟩ := h₁ αX αY (e.inv ≫ f) (by simp [hX]) (by simp [hY])
case mp.intro.intro.left
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
X✝ Y✝ X Y : C
c : BinaryCofan X Y
cofans : (X Y : C) → BinaryCofan X Y
colimits : (X Y : C) → IsColimit (cofans X Y)
cones : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → PullbackCone f g
limits : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → IsLimit (cones f g)
h₁ :
  ∀ {X' Y' : C} (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : (cofans X' Y').pt ⟶ c.pt),
    αX ≫ BinaryCofan.inl c = BinaryCofan.inl (cofans X' Y') ≫ f →
      αY ≫ BinaryCofan.inr c = BinaryCofan.inr (cofans X' Y') ≫ f →
        IsPullback (BinaryCofan.inl (cofans X' Y')) αX f (BinaryCofan.inl c) ∧
          IsPullback (BinaryCofan.inr (cofans X' Y')) αY f (BinaryCofan.inr c)
h₂ :
  {Z : C} →
    (f : Z ⟶ c.pt) →
      IsColimit
        (BinaryCofan.mk (PullbackCone.fst (cones f (BinaryCofan.inl c)))
          (PullbackCone.fst (cones f (BinaryCofan.inr c))))
X' Y' : C
c' : BinaryCofan X' Y'
αX : X' ⟶ X
αY : Y' ⟶ Y
f : c'.pt ⟶ c.pt
hX : αX ≫ BinaryCofan.inl c = BinaryCofan.inl c' ≫ f
hY : αY ≫ BinaryCofan.inr c = BinaryCofan.inr c' ≫ f
h : IsColimit c'
e : c'.pt ≅ (cofans X' Y').pt := IsColimit.coconePointUniqueUpToIso h (colimits X' Y')
hl : IsPullback (BinaryCofan.inl (cofans X' Y')) αX (e.inv ≫ f) (BinaryCofan.inl c)
hr : IsPullback (BinaryCofan.inr (cofans X' Y')) αY (e.inv ≫ f) (BinaryCofan.inr c)
⊢ IsPullback (BinaryCofan.inl c') αX f (BinaryCofan.inl c)

case mp.intro.intro.right
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
X✝ Y✝ X Y : C
c : BinaryCofan X Y
cofans : (X Y : C) → BinaryCofan X Y
colimits : (X Y : C) → IsColimit (cofans X Y)
cones : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → PullbackCone f g
limits : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → IsLimit (cones f g)
h₁ :
  ∀ {X' Y' : C} (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : (cofans X' Y').pt ⟶ c.pt),
    αX ≫ BinaryCofan.inl c = BinaryCofan.inl (cofans X' Y') ≫ f →
      αY ≫ BinaryCofan.inr c = BinaryCofan.inr (cofans X' Y') ≫ f →
        IsPullback (BinaryCofan.inl (cofans X' Y')) αX f (BinaryCofan.inl c) ∧
          IsPullback (BinaryCofan.inr (cofans X' Y')) αY f (BinaryCofan.inr c)
h₂ :
  {Z : C} →
    (f : Z ⟶ c.pt) →
      IsColimit
        (BinaryCofan.mk (PullbackCone.fst (cones f (BinaryCofan.inl c)))
          (PullbackCone.fst (cones f (BinaryCofan.inr c))))
X' Y' : C
c' : BinaryCofan X' Y'
αX : X' ⟶ X
αY : Y' ⟶ Y
f : c'.pt ⟶ c.pt
hX : αX ≫ BinaryCofan.inl c = BinaryCofan.inl c' ≫ f
hY : αY ≫ BinaryCofan.inr c = BinaryCofan.inr c' ≫ f
h : IsColimit c'
e : c'.pt ≅ (cofans X' Y').pt := IsColimit.coconePointUniqueUpToIso h (colimits X' Y')
hl : IsPullback (BinaryCofan.inl (cofans X' Y')) αX (e.inv ≫ f) (BinaryCofan.inl c)
hr : IsPullback (BinaryCofan.inr (cofans X' Y')) αY (e.inv ≫ f) (BinaryCofan.inr c)
⊢ IsPullback (BinaryCofan.inr c') αY f (BinaryCofan.inr c)
case mp.intro.intro
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
X✝ Y✝ X Y : C
c : BinaryCofan X Y
cofans : (X Y : C) → BinaryCofan X Y
colimits : (X Y : C) → IsColimit (cofans X Y)
cones : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → PullbackCone f g
limits : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → IsLimit (cones f g)
h₁ :
  ∀ {X' Y' : C} (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : (cofans X' Y').pt ⟶ c.pt),
    αX ≫ BinaryCofan.inl c = BinaryCofan.inl (cofans X' Y') ≫ f →
      αY ≫ BinaryCofan.inr c = BinaryCofan.inr (cofans X' Y') ≫ f →
        IsPullback (BinaryCofan.inl (cofans X' Y')) αX f (BinaryCofan.inl c) ∧
          IsPullback (BinaryCofan.inr (cofans X' Y')) αY f (BinaryCofan.inr c)
h₂ :
  {Z : C} →
    (f : Z ⟶ c.pt) →
      IsColimit
        (BinaryCofan.mk (PullbackCone.fst (cones f (BinaryCofan.inl c)))
          (PullbackCone.fst (cones f (BinaryCofan.inr c))))
X' Y' : C
c' : BinaryCofan X' Y'
αX : X' ⟶ X
αY : Y' ⟶ Y
f : c'.pt ⟶ c.pt
hX : αX ≫ BinaryCofan.inl c = BinaryCofan.inl c' ≫ f
hY : αY ≫ BinaryCofan.inr c = BinaryCofan.inr c' ≫ f
h : IsColimit c'
e : c'.pt ≅ (cofans X' Y').pt := IsColimit.coconePointUniqueUpToIso h (colimits X' Y')
hl : IsPullback (BinaryCofan.inl (cofans X' Y')) αX (e.inv ≫ f) (BinaryCofan.inl c)
hr : IsPullback (BinaryCofan.inr (cofans X' Y')) αY (e.inv ≫ f) (BinaryCofan.inr c)
⊢ IsPullback (BinaryCofan.inl c') αX f (BinaryCofan.inl c) ∧ IsPullback (BinaryCofan.inr c') αY f (BinaryCofan.inr c)
constructor
no goals
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
X✝ Y✝ X Y : C
c : BinaryCofan X Y
cofans : (X Y : C) → BinaryCofan X Y
colimits : (X Y : C) → IsColimit (cofans X Y)
cones : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → PullbackCone f g
limits : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → IsLimit (cones f g)
h₁ :
  ∀ {X' Y' : C} (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : (cofans X' Y').pt ⟶ c.pt),
    αX ≫ BinaryCofan.inl c = BinaryCofan.inl (cofans X' Y') ≫ f →
      αY ≫ BinaryCofan.inr c = BinaryCofan.inr (cofans X' Y') ≫ f →
        IsPullback (BinaryCofan.inl (cofans X' Y')) αX f (BinaryCofan.inl c) ∧
          IsPullback (BinaryCofan.inr (cofans X' Y')) αY f (BinaryCofan.inr c)
h₂ :
  {Z : C} →
    (f : Z ⟶ c.pt) →
      IsColimit
        (BinaryCofan.mk (PullbackCone.fst (cones f (BinaryCofan.inl c)))
          (PullbackCone.fst (cones f (BinaryCofan.inr c))))
X' Y' : C
c' : BinaryCofan X' Y'
αX : X' ⟶ X
αY : Y' ⟶ Y
f : c'.pt ⟶ c.pt
hX : αX ≫ BinaryCofan.inl c = BinaryCofan.inl c' ≫ f
hY : αY ≫ BinaryCofan.inr c = BinaryCofan.inr c' ≫ f
h : IsColimit c'
e : c'.pt ≅ (cofans X' Y').pt := IsColimit.coconePointUniqueUpToIso h (colimits X' Y')
⊢ αX ≫ BinaryCofan.inl c = BinaryCofan.inl (cofans X' Y') ≫ e.inv ≫ f
simp [hX]
no goals
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
X✝ Y✝ X Y : C
c : BinaryCofan X Y
cofans : (X Y : C) → BinaryCofan X Y
colimits : (X Y : C) → IsColimit (cofans X Y)
cones : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → PullbackCone f g
limits : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → IsLimit (cones f g)
h₁ :
  ∀ {X' Y' : C} (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : (cofans X' Y').pt ⟶ c.pt),
    αX ≫ BinaryCofan.inl c = BinaryCofan.inl (cofans X' Y') ≫ f →
      αY ≫ BinaryCofan.inr c = BinaryCofan.inr (cofans X' Y') ≫ f →
        IsPullback (BinaryCofan.inl (cofans X' Y')) αX f (BinaryCofan.inl c) ∧
          IsPullback (BinaryCofan.inr (cofans X' Y')) αY f (BinaryCofan.inr c)
h₂ :
  {Z : C} →
    (f : Z ⟶ c.pt) →
      IsColimit
        (BinaryCofan.mk (PullbackCone.fst (cones f (BinaryCofan.inl c)))
          (PullbackCone.fst (cones f (BinaryCofan.inr c))))
X' Y' : C
c' : BinaryCofan X' Y'
αX : X' ⟶ X
αY : Y' ⟶ Y
f : c'.pt ⟶ c.pt
hX : αX ≫ BinaryCofan.inl c = BinaryCofan.inl c' ≫ f
hY : αY ≫ BinaryCofan.inr c = BinaryCofan.inr c' ≫ f
h : IsColimit c'
e : c'.pt ≅ (cofans X' Y').pt := IsColimit.coconePointUniqueUpToIso h (colimits X' Y')
⊢ αY ≫ BinaryCofan.inr c = BinaryCofan.inr (cofans X' Y') ≫ e.inv ≫ f
simp [hY]
case mp.intro.intro.left
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
X✝ Y✝ X Y : C
c : BinaryCofan X Y
cofans : (X Y : C) → BinaryCofan X Y
colimits : (X Y : C) → IsColimit (cofans X Y)
cones : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → PullbackCone f g
limits : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → IsLimit (cones f g)
h₁ :
  ∀ {X' Y' : C} (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : (cofans X' Y').pt ⟶ c.pt),
    αX ≫ BinaryCofan.inl c = BinaryCofan.inl (cofans X' Y') ≫ f →
      αY ≫ BinaryCofan.inr c = BinaryCofan.inr (cofans X' Y') ≫ f →
        IsPullback (BinaryCofan.inl (cofans X' Y')) αX f (BinaryCofan.inl c) ∧
          IsPullback (BinaryCofan.inr (cofans X' Y')) αY f (BinaryCofan.inr c)
h₂ :
  {Z : C} →
    (f : Z ⟶ c.pt) →
      IsColimit
        (BinaryCofan.mk (PullbackCone.fst (cones f (BinaryCofan.inl c)))
          (PullbackCone.fst (cones f (BinaryCofan.inr c))))
X' Y' : C
c' : BinaryCofan X' Y'
αX : X' ⟶ X
αY : Y' ⟶ Y
f : c'.pt ⟶ c.pt
hX : αX ≫ BinaryCofan.inl c = BinaryCofan.inl c' ≫ f
hY : αY ≫ BinaryCofan.inr c = BinaryCofan.inr c' ≫ f
h : IsColimit c'
e : c'.pt ≅ (cofans X' Y').pt := IsColimit.coconePointUniqueUpToIso h (colimits X' Y')
hl : IsPullback (BinaryCofan.inl (cofans X' Y')) αX (e.inv ≫ f) (BinaryCofan.inl c)
hr : IsPullback (BinaryCofan.inr (cofans X' Y')) αY (e.inv ≫ f) (BinaryCofan.inr c)
⊢ IsPullback (BinaryCofan.inl c') (𝟙 X' ≫ αX) (e.hom ≫ e.inv ≫ f) (BinaryCofan.inl c)
case mp.intro.intro.left
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
X✝ Y✝ X Y : C
c : BinaryCofan X Y
cofans : (X Y : C) → BinaryCofan X Y
colimits : (X Y : C) → IsColimit (cofans X Y)
cones : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → PullbackCone f g
limits : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → IsLimit (cones f g)
h₁ :
  ∀ {X' Y' : C} (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : (cofans X' Y').pt ⟶ c.pt),
    αX ≫ BinaryCofan.inl c = BinaryCofan.inl (cofans X' Y') ≫ f →
      αY ≫ BinaryCofan.inr c = BinaryCofan.inr (cofans X' Y') ≫ f →
        IsPullback (BinaryCofan.inl (cofans X' Y')) αX f (BinaryCofan.inl c) ∧
          IsPullback (BinaryCofan.inr (cofans X' Y')) αY f (BinaryCofan.inr c)
h₂ :
  {Z : C} →
    (f : Z ⟶ c.pt) →
      IsColimit
        (BinaryCofan.mk (PullbackCone.fst (cones f (BinaryCofan.inl c)))
          (PullbackCone.fst (cones f (BinaryCofan.inr c))))
X' Y' : C
c' : BinaryCofan X' Y'
αX : X' ⟶ X
αY : Y' ⟶ Y
f : c'.pt ⟶ c.pt
hX : αX ≫ BinaryCofan.inl c = BinaryCofan.inl c' ≫ f
hY : αY ≫ BinaryCofan.inr c = BinaryCofan.inr c' ≫ f
h : IsColimit c'
e : c'.pt ≅ (cofans X' Y').pt := IsColimit.coconePointUniqueUpToIso h (colimits X' Y')
hl : IsPullback (BinaryCofan.inl (cofans X' Y')) αX (e.inv ≫ f) (BinaryCofan.inl c)
hr : IsPullback (BinaryCofan.inr (cofans X' Y')) αY (e.inv ≫ f) (BinaryCofan.inr c)
⊢ IsPullback (BinaryCofan.inl c') αX f (BinaryCofan.inl c)
rw [← Category.id_comp αX, ← Iso.hom_inv_id_assoc e f]
case mp.intro.intro.left
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
X✝ Y✝ X Y : C
c : BinaryCofan X Y
cofans : (X Y : C) → BinaryCofan X Y
colimits : (X Y : C) → IsColimit (cofans X Y)
cones : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → PullbackCone f g
limits : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → IsLimit (cones f g)
h₁ :
  ∀ {X' Y' : C} (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : (cofans X' Y').pt ⟶ c.pt),
    αX ≫ BinaryCofan.inl c = BinaryCofan.inl (cofans X' Y') ≫ f →
      αY ≫ BinaryCofan.inr c = BinaryCofan.inr (cofans X' Y') ≫ f →
        IsPullback (BinaryCofan.inl (cofans X' Y')) αX f (BinaryCofan.inl c) ∧
          IsPullback (BinaryCofan.inr (cofans X' Y')) αY f (BinaryCofan.inr c)
h₂ :
  {Z : C} →
    (f : Z ⟶ c.pt) →
      IsColimit
        (BinaryCofan.mk (PullbackCone.fst (cones f (BinaryCofan.inl c)))
          (PullbackCone.fst (cones f (BinaryCofan.inr c))))
X' Y' : C
c' : BinaryCofan X' Y'
αX : X' ⟶ X
αY : Y' ⟶ Y
f : c'.pt ⟶ c.pt
hX : αX ≫ BinaryCofan.inl c = BinaryCofan.inl c' ≫ f
hY : αY ≫ BinaryCofan.inr c = BinaryCofan.inr c' ≫ f
h : IsColimit c'
e : c'.pt ≅ (cofans X' Y').pt := IsColimit.coconePointUniqueUpToIso h (colimits X' Y')
hl : IsPullback (BinaryCofan.inl (cofans X' Y')) αX (e.inv ≫ f) (BinaryCofan.inl c)
hr : IsPullback (BinaryCofan.inr (cofans X' Y')) αY (e.inv ≫ f) (BinaryCofan.inr c)
this : IsIso (𝟙 X')
⊢ IsPullback (BinaryCofan.inl c') (𝟙 X' ≫ αX) (e.hom ≫ e.inv ≫ f) (BinaryCofan.inl c)
case mp.intro.intro.left
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
X✝ Y✝ X Y : C
c : BinaryCofan X Y
cofans : (X Y : C) → BinaryCofan X Y
colimits : (X Y : C) → IsColimit (cofans X Y)
cones : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → PullbackCone f g
limits : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → IsLimit (cones f g)
h₁ :
  ∀ {X' Y' : C} (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : (cofans X' Y').pt ⟶ c.pt),
    αX ≫ BinaryCofan.inl c = BinaryCofan.inl (cofans X' Y') ≫ f →
      αY ≫ BinaryCofan.inr c = BinaryCofan.inr (cofans X' Y') ≫ f →
        IsPullback (BinaryCofan.inl (cofans X' Y')) αX f (BinaryCofan.inl c) ∧
          IsPullback (BinaryCofan.inr (cofans X' Y')) αY f (BinaryCofan.inr c)
h₂ :
  {Z : C} →
    (f : Z ⟶ c.pt) →
      IsColimit
        (BinaryCofan.mk (PullbackCone.fst (cones f (BinaryCofan.inl c)))
          (PullbackCone.fst (cones f (BinaryCofan.inr c))))
X' Y' : C
c' : BinaryCofan X' Y'
αX : X' ⟶ X
αY : Y' ⟶ Y
f : c'.pt ⟶ c.pt
hX : αX ≫ BinaryCofan.inl c = BinaryCofan.inl c' ≫ f
hY : αY ≫ BinaryCofan.inr c = BinaryCofan.inr c' ≫ f
h : IsColimit c'
e : c'.pt ≅ (cofans X' Y').pt := IsColimit.coconePointUniqueUpToIso h (colimits X' Y')
hl : IsPullback (BinaryCofan.inl (cofans X' Y')) αX (e.inv ≫ f) (BinaryCofan.inl c)
hr : IsPullback (BinaryCofan.inr (cofans X' Y')) αY (e.inv ≫ f) (BinaryCofan.inr c)
⊢ IsPullback (BinaryCofan.inl c') (𝟙 X' ≫ αX) (e.hom ≫ e.inv ≫ f) (BinaryCofan.inl c)
haveI : IsIso (𝟙 X') := inferInstance
case mp.intro.intro.left
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
X✝ Y✝ X Y : C
c : BinaryCofan X Y
cofans : (X Y : C) → BinaryCofan X Y
colimits : (X Y : C) → IsColimit (cofans X Y)
cones : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → PullbackCone f g
limits : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → IsLimit (cones f g)
h₁ :
  ∀ {X' Y' : C} (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : (cofans X' Y').pt ⟶ c.pt),
    αX ≫ BinaryCofan.inl c = BinaryCofan.inl (cofans X' Y') ≫ f →
      αY ≫ BinaryCofan.inr c = BinaryCofan.inr (cofans X' Y') ≫ f →
        IsPullback (BinaryCofan.inl (cofans X' Y')) αX f (BinaryCofan.inl c) ∧
          IsPullback (BinaryCofan.inr (cofans X' Y')) αY f (BinaryCofan.inr c)
h₂ :
  {Z : C} →
    (f : Z ⟶ c.pt) →
      IsColimit
        (BinaryCofan.mk (PullbackCone.fst (cones f (BinaryCofan.inl c)))
          (PullbackCone.fst (cones f (BinaryCofan.inr c))))
X' Y' : C
c' : BinaryCofan X' Y'
αX : X' ⟶ X
αY : Y' ⟶ Y
f : c'.pt ⟶ c.pt
hX : αX ≫ BinaryCofan.inl c = BinaryCofan.inl c' ≫ f
hY : αY ≫ BinaryCofan.inr c = BinaryCofan.inr c' ≫ f
h : IsColimit c'
e : c'.pt ≅ (cofans X' Y').pt := IsColimit.coconePointUniqueUpToIso h (colimits X' Y')
hl : IsPullback (BinaryCofan.inl (cofans X' Y')) αX (e.inv ≫ f) (BinaryCofan.inl c)
hr : IsPullback (BinaryCofan.inr (cofans X' Y')) αY (e.inv ≫ f) (BinaryCofan.inr c)
this✝ : IsIso (𝟙 X')
this : BinaryCofan.inl c' ≫ e.hom = 𝟙 X' ≫ BinaryCofan.inl (cofans X' Y')
⊢ IsPullback (BinaryCofan.inl c') (𝟙 X' ≫ αX) (e.hom ≫ e.inv ≫ f) (BinaryCofan.inl c)
case mp.intro.intro.left
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
X✝ Y✝ X Y : C
c : BinaryCofan X Y
cofans : (X Y : C) → BinaryCofan X Y
colimits : (X Y : C) → IsColimit (cofans X Y)
cones : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → PullbackCone f g
limits : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → IsLimit (cones f g)
h₁ :
  ∀ {X' Y' : C} (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : (cofans X' Y').pt ⟶ c.pt),
    αX ≫ BinaryCofan.inl c = BinaryCofan.inl (cofans X' Y') ≫ f →
      αY ≫ BinaryCofan.inr c = BinaryCofan.inr (cofans X' Y') ≫ f →
        IsPullback (BinaryCofan.inl (cofans X' Y')) αX f (BinaryCofan.inl c) ∧
          IsPullback (BinaryCofan.inr (cofans X' Y')) αY f (BinaryCofan.inr c)
h₂ :
  {Z : C} →
    (f : Z ⟶ c.pt) →
      IsColimit
        (BinaryCofan.mk (PullbackCone.fst (cones f (BinaryCofan.inl c)))
          (PullbackCone.fst (cones f (BinaryCofan.inr c))))
X' Y' : C
c' : BinaryCofan X' Y'
αX : X' ⟶ X
αY : Y' ⟶ Y
f : c'.pt ⟶ c.pt
hX : αX ≫ BinaryCofan.inl c = BinaryCofan.inl c' ≫ f
hY : αY ≫ BinaryCofan.inr c = BinaryCofan.inr c' ≫ f
h : IsColimit c'
e : c'.pt ≅ (cofans X' Y').pt := IsColimit.coconePointUniqueUpToIso h (colimits X' Y')
hl : IsPullback (BinaryCofan.inl (cofans X' Y')) αX (e.inv ≫ f) (BinaryCofan.inl c)
hr : IsPullback (BinaryCofan.inr (cofans X' Y')) αY (e.inv ≫ f) (BinaryCofan.inr c)
this : IsIso (𝟙 X')
⊢ IsPullback (BinaryCofan.inl c') (𝟙 X' ≫ αX) (e.hom ≫ e.inv ≫ f) (BinaryCofan.inl c)
have : c'.inl ≫ e.hom = 𝟙 X' ≫ (cofans X' Y').inl := by
  dsimp
  simp
no goals
case mp.intro.intro.left
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
X✝ Y✝ X Y : C
c : BinaryCofan X Y
cofans : (X Y : C) → BinaryCofan X Y
colimits : (X Y : C) → IsColimit (cofans X Y)
cones : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → PullbackCone f g
limits : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → IsLimit (cones f g)
h₁ :
  ∀ {X' Y' : C} (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : (cofans X' Y').pt ⟶ c.pt),
    αX ≫ BinaryCofan.inl c = BinaryCofan.inl (cofans X' Y') ≫ f →
      αY ≫ BinaryCofan.inr c = BinaryCofan.inr (cofans X' Y') ≫ f →
        IsPullback (BinaryCofan.inl (cofans X' Y')) αX f (BinaryCofan.inl c) ∧
          IsPullback (BinaryCofan.inr (cofans X' Y')) αY f (BinaryCofan.inr c)
h₂ :
  {Z : C} →
    (f : Z ⟶ c.pt) →
      IsColimit
        (BinaryCofan.mk (PullbackCone.fst (cones f (BinaryCofan.inl c)))
          (PullbackCone.fst (cones f (BinaryCofan.inr c))))
X' Y' : C
c' : BinaryCofan X' Y'
αX : X' ⟶ X
αY : Y' ⟶ Y
f : c'.pt ⟶ c.pt
hX : αX ≫ BinaryCofan.inl c = BinaryCofan.inl c' ≫ f
hY : αY ≫ BinaryCofan.inr c = BinaryCofan.inr c' ≫ f
h : IsColimit c'
e : c'.pt ≅ (cofans X' Y').pt := IsColimit.coconePointUniqueUpToIso h (colimits X' Y')
hl : IsPullback (BinaryCofan.inl (cofans X' Y')) αX (e.inv ≫ f) (BinaryCofan.inl c)
hr : IsPullback (BinaryCofan.inr (cofans X' Y')) αY (e.inv ≫ f) (BinaryCofan.inr c)
this✝ : IsIso (𝟙 X')
this : BinaryCofan.inl c' ≫ e.hom = 𝟙 X' ≫ BinaryCofan.inl (cofans X' Y')
⊢ IsPullback (BinaryCofan.inl c') (𝟙 X' ≫ αX) (e.hom ≫ e.inv ≫ f) (BinaryCofan.inl c)
exact (IsPullback.of_vert_isIso ⟨this⟩).paste_vert hl
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
X✝ Y✝ X Y : C
c : BinaryCofan X Y
cofans : (X Y : C) → BinaryCofan X Y
colimits : (X Y : C) → IsColimit (cofans X Y)
cones : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → PullbackCone f g
limits : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → IsLimit (cones f g)
h₁ :
  ∀ {X' Y' : C} (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : (cofans X' Y').pt ⟶ c.pt),
    αX ≫ BinaryCofan.inl c = BinaryCofan.inl (cofans X' Y') ≫ f →
      αY ≫ BinaryCofan.inr c = BinaryCofan.inr (cofans X' Y') ≫ f →
        IsPullback (BinaryCofan.inl (cofans X' Y')) αX f (BinaryCofan.inl c) ∧
          IsPullback (BinaryCofan.inr (cofans X' Y')) αY f (BinaryCofan.inr c)
h₂ :
  {Z : C} →
    (f : Z ⟶ c.pt) →
      IsColimit
        (BinaryCofan.mk (PullbackCone.fst (cones f (BinaryCofan.inl c)))
          (PullbackCone.fst (cones f (BinaryCofan.inr c))))
X' Y' : C
c' : BinaryCofan X' Y'
αX : X' ⟶ X
αY : Y' ⟶ Y
f : c'.pt ⟶ c.pt
hX : αX ≫ BinaryCofan.inl c = BinaryCofan.inl c' ≫ f
hY : αY ≫ BinaryCofan.inr c = BinaryCofan.inr c' ≫ f
h : IsColimit c'
e : c'.pt ≅ (cofans X' Y').pt := IsColimit.coconePointUniqueUpToIso h (colimits X' Y')
hl : IsPullback (BinaryCofan.inl (cofans X' Y')) αX (e.inv ≫ f) (BinaryCofan.inl c)
hr : IsPullback (BinaryCofan.inr (cofans X' Y')) αY (e.inv ≫ f) (BinaryCofan.inr c)
this : IsIso (𝟙 X')
⊢ BinaryCofan.inl c' ≫ (IsColimit.coconePointUniqueUpToIso h (colimits X' Y')).hom =
    𝟙 X' ≫ BinaryCofan.inl (cofans X' Y')
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
X✝ Y✝ X Y : C
c : BinaryCofan X Y
cofans : (X Y : C) → BinaryCofan X Y
colimits : (X Y : C) → IsColimit (cofans X Y)
cones : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → PullbackCone f g
limits : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → IsLimit (cones f g)
h₁ :
  ∀ {X' Y' : C} (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : (cofans X' Y').pt ⟶ c.pt),
    αX ≫ BinaryCofan.inl c = BinaryCofan.inl (cofans X' Y') ≫ f →
      αY ≫ BinaryCofan.inr c = BinaryCofan.inr (cofans X' Y') ≫ f →
        IsPullback (BinaryCofan.inl (cofans X' Y')) αX f (BinaryCofan.inl c) ∧
          IsPullback (BinaryCofan.inr (cofans X' Y')) αY f (BinaryCofan.inr c)
h₂ :
  {Z : C} →
    (f : Z ⟶ c.pt) →
      IsColimit
        (BinaryCofan.mk (PullbackCone.fst (cones f (BinaryCofan.inl c)))
          (PullbackCone.fst (cones f (BinaryCofan.inr c))))
X' Y' : C
c' : BinaryCofan X' Y'
αX : X' ⟶ X
αY : Y' ⟶ Y
f : c'.pt ⟶ c.pt
hX : αX ≫ BinaryCofan.inl c = BinaryCofan.inl c' ≫ f
hY : αY ≫ BinaryCofan.inr c = BinaryCofan.inr c' ≫ f
h : IsColimit c'
e : c'.pt ≅ (cofans X' Y').pt := IsColimit.coconePointUniqueUpToIso h (colimits X' Y')
hl : IsPullback (BinaryCofan.inl (cofans X' Y')) αX (e.inv ≫ f) (BinaryCofan.inl c)
hr : IsPullback (BinaryCofan.inr (cofans X' Y')) αY (e.inv ≫ f) (BinaryCofan.inr c)
this : IsIso (𝟙 X')
⊢ BinaryCofan.inl c' ≫ e.hom = 𝟙 X' ≫ BinaryCofan.inl (cofans X' Y')
dsimp
no goals
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
X✝ Y✝ X Y : C
c : BinaryCofan X Y
cofans : (X Y : C) → BinaryCofan X Y
colimits : (X Y : C) → IsColimit (cofans X Y)
cones : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → PullbackCone f g
limits : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → IsLimit (cones f g)
h₁ :
  ∀ {X' Y' : C} (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : (cofans X' Y').pt ⟶ c.pt),
    αX ≫ BinaryCofan.inl c = BinaryCofan.inl (cofans X' Y') ≫ f →
      αY ≫ BinaryCofan.inr c = BinaryCofan.inr (cofans X' Y') ≫ f →
        IsPullback (BinaryCofan.inl (cofans X' Y')) αX f (BinaryCofan.inl c) ∧
          IsPullback (BinaryCofan.inr (cofans X' Y')) αY f (BinaryCofan.inr c)
h₂ :
  {Z : C} →
    (f : Z ⟶ c.pt) →
      IsColimit
        (BinaryCofan.mk (PullbackCone.fst (cones f (BinaryCofan.inl c)))
          (PullbackCone.fst (cones f (BinaryCofan.inr c))))
X' Y' : C
c' : BinaryCofan X' Y'
αX : X' ⟶ X
αY : Y' ⟶ Y
f : c'.pt ⟶ c.pt
hX : αX ≫ BinaryCofan.inl c = BinaryCofan.inl c' ≫ f
hY : αY ≫ BinaryCofan.inr c = BinaryCofan.inr c' ≫ f
h : IsColimit c'
e : c'.pt ≅ (cofans X' Y').pt := IsColimit.coconePointUniqueUpToIso h (colimits X' Y')
hl : IsPullback (BinaryCofan.inl (cofans X' Y')) αX (e.inv ≫ f) (BinaryCofan.inl c)
hr : IsPullback (BinaryCofan.inr (cofans X' Y')) αY (e.inv ≫ f) (BinaryCofan.inr c)
this : IsIso (𝟙 X')
⊢ BinaryCofan.inl c' ≫ (IsColimit.coconePointUniqueUpToIso h (colimits X' Y')).hom =
    𝟙 X' ≫ BinaryCofan.inl (cofans X' Y')
simp
case mp.intro.intro.right
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
X✝ Y✝ X Y : C
c : BinaryCofan X Y
cofans : (X Y : C) → BinaryCofan X Y
colimits : (X Y : C) → IsColimit (cofans X Y)
cones : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → PullbackCone f g
limits : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → IsLimit (cones f g)
h₁ :
  ∀ {X' Y' : C} (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : (cofans X' Y').pt ⟶ c.pt),
    αX ≫ BinaryCofan.inl c = BinaryCofan.inl (cofans X' Y') ≫ f →
      αY ≫ BinaryCofan.inr c = BinaryCofan.inr (cofans X' Y') ≫ f →
        IsPullback (BinaryCofan.inl (cofans X' Y')) αX f (BinaryCofan.inl c) ∧
          IsPullback (BinaryCofan.inr (cofans X' Y')) αY f (BinaryCofan.inr c)
h₂ :
  {Z : C} →
    (f : Z ⟶ c.pt) →
      IsColimit
        (BinaryCofan.mk (PullbackCone.fst (cones f (BinaryCofan.inl c)))
          (PullbackCone.fst (cones f (BinaryCofan.inr c))))
X' Y' : C
c' : BinaryCofan X' Y'
αX : X' ⟶ X
αY : Y' ⟶ Y
f : c'.pt ⟶ c.pt
hX : αX ≫ BinaryCofan.inl c = BinaryCofan.inl c' ≫ f
hY : αY ≫ BinaryCofan.inr c = BinaryCofan.inr c' ≫ f
h : IsColimit c'
e : c'.pt ≅ (cofans X' Y').pt := IsColimit.coconePointUniqueUpToIso h (colimits X' Y')
hl : IsPullback (BinaryCofan.inl (cofans X' Y')) αX (e.inv ≫ f) (BinaryCofan.inl c)
hr : IsPullback (BinaryCofan.inr (cofans X' Y')) αY (e.inv ≫ f) (BinaryCofan.inr c)
⊢ IsPullback (BinaryCofan.inr c') (𝟙 Y' ≫ αY) (e.hom ≫ e.inv ≫ f) (BinaryCofan.inr c)
case mp.intro.intro.right
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
X✝ Y✝ X Y : C
c : BinaryCofan X Y
cofans : (X Y : C) → BinaryCofan X Y
colimits : (X Y : C) → IsColimit (cofans X Y)
cones : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → PullbackCone f g
limits : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → IsLimit (cones f g)
h₁ :
  ∀ {X' Y' : C} (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : (cofans X' Y').pt ⟶ c.pt),
    αX ≫ BinaryCofan.inl c = BinaryCofan.inl (cofans X' Y') ≫ f →
      αY ≫ BinaryCofan.inr c = BinaryCofan.inr (cofans X' Y') ≫ f →
        IsPullback (BinaryCofan.inl (cofans X' Y')) αX f (BinaryCofan.inl c) ∧
          IsPullback (BinaryCofan.inr (cofans X' Y')) αY f (BinaryCofan.inr c)
h₂ :
  {Z : C} →
    (f : Z ⟶ c.pt) →
      IsColimit
        (BinaryCofan.mk (PullbackCone.fst (cones f (BinaryCofan.inl c)))
          (PullbackCone.fst (cones f (BinaryCofan.inr c))))
X' Y' : C
c' : BinaryCofan X' Y'
αX : X' ⟶ X
αY : Y' ⟶ Y
f : c'.pt ⟶ c.pt
hX : αX ≫ BinaryCofan.inl c = BinaryCofan.inl c' ≫ f
hY : αY ≫ BinaryCofan.inr c = BinaryCofan.inr c' ≫ f
h : IsColimit c'
e : c'.pt ≅ (cofans X' Y').pt := IsColimit.coconePointUniqueUpToIso h (colimits X' Y')
hl : IsPullback (BinaryCofan.inl (cofans X' Y')) αX (e.inv ≫ f) (BinaryCofan.inl c)
hr : IsPullback (BinaryCofan.inr (cofans X' Y')) αY (e.inv ≫ f) (BinaryCofan.inr c)
⊢ IsPullback (BinaryCofan.inr c') αY f (BinaryCofan.inr c)
rw [← Category.id_comp αY, ← Iso.hom_inv_id_assoc e f]
case mp.intro.intro.right
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
X✝ Y✝ X Y : C
c : BinaryCofan X Y
cofans : (X Y : C) → BinaryCofan X Y
colimits : (X Y : C) → IsColimit (cofans X Y)
cones : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → PullbackCone f g
limits : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → IsLimit (cones f g)
h₁ :
  ∀ {X' Y' : C} (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : (cofans X' Y').pt ⟶ c.pt),
    αX ≫ BinaryCofan.inl c = BinaryCofan.inl (cofans X' Y') ≫ f →
      αY ≫ BinaryCofan.inr c = BinaryCofan.inr (cofans X' Y') ≫ f →
        IsPullback (BinaryCofan.inl (cofans X' Y')) αX f (BinaryCofan.inl c) ∧
          IsPullback (BinaryCofan.inr (cofans X' Y')) αY f (BinaryCofan.inr c)
h₂ :
  {Z : C} →
    (f : Z ⟶ c.pt) →
      IsColimit
        (BinaryCofan.mk (PullbackCone.fst (cones f (BinaryCofan.inl c)))
          (PullbackCone.fst (cones f (BinaryCofan.inr c))))
X' Y' : C
c' : BinaryCofan X' Y'
αX : X' ⟶ X
αY : Y' ⟶ Y
f : c'.pt ⟶ c.pt
hX : αX ≫ BinaryCofan.inl c = BinaryCofan.inl c' ≫ f
hY : αY ≫ BinaryCofan.inr c = BinaryCofan.inr c' ≫ f
h : IsColimit c'
e : c'.pt ≅ (cofans X' Y').pt := IsColimit.coconePointUniqueUpToIso h (colimits X' Y')
hl : IsPullback (BinaryCofan.inl (cofans X' Y')) αX (e.inv ≫ f) (BinaryCofan.inl c)
hr : IsPullback (BinaryCofan.inr (cofans X' Y')) αY (e.inv ≫ f) (BinaryCofan.inr c)
this : IsIso (𝟙 Y')
⊢ IsPullback (BinaryCofan.inr c') (𝟙 Y' ≫ αY) (e.hom ≫ e.inv ≫ f) (BinaryCofan.inr c)
case mp.intro.intro.right
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
X✝ Y✝ X Y : C
c : BinaryCofan X Y
cofans : (X Y : C) → BinaryCofan X Y
colimits : (X Y : C) → IsColimit (cofans X Y)
cones : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → PullbackCone f g
limits : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → IsLimit (cones f g)
h₁ :
  ∀ {X' Y' : C} (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : (cofans X' Y').pt ⟶ c.pt),
    αX ≫ BinaryCofan.inl c = BinaryCofan.inl (cofans X' Y') ≫ f →
      αY ≫ BinaryCofan.inr c = BinaryCofan.inr (cofans X' Y') ≫ f →
        IsPullback (BinaryCofan.inl (cofans X' Y')) αX f (BinaryCofan.inl c) ∧
          IsPullback (BinaryCofan.inr (cofans X' Y')) αY f (BinaryCofan.inr c)
h₂ :
  {Z : C} →
    (f : Z ⟶ c.pt) →
      IsColimit
        (BinaryCofan.mk (PullbackCone.fst (cones f (BinaryCofan.inl c)))
          (PullbackCone.fst (cones f (BinaryCofan.inr c))))
X' Y' : C
c' : BinaryCofan X' Y'
αX : X' ⟶ X
αY : Y' ⟶ Y
f : c'.pt ⟶ c.pt
hX : αX ≫ BinaryCofan.inl c = BinaryCofan.inl c' ≫ f
hY : αY ≫ BinaryCofan.inr c = BinaryCofan.inr c' ≫ f
h : IsColimit c'
e : c'.pt ≅ (cofans X' Y').pt := IsColimit.coconePointUniqueUpToIso h (colimits X' Y')
hl : IsPullback (BinaryCofan.inl (cofans X' Y')) αX (e.inv ≫ f) (BinaryCofan.inl c)
hr : IsPullback (BinaryCofan.inr (cofans X' Y')) αY (e.inv ≫ f) (BinaryCofan.inr c)
⊢ IsPullback (BinaryCofan.inr c') (𝟙 Y' ≫ αY) (e.hom ≫ e.inv ≫ f) (BinaryCofan.inr c)
haveI : IsIso (𝟙 Y') := inferInstance
case mp.intro.intro.right
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
X✝ Y✝ X Y : C
c : BinaryCofan X Y
cofans : (X Y : C) → BinaryCofan X Y
colimits : (X Y : C) → IsColimit (cofans X Y)
cones : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → PullbackCone f g
limits : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → IsLimit (cones f g)
h₁ :
  ∀ {X' Y' : C} (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : (cofans X' Y').pt ⟶ c.pt),
    αX ≫ BinaryCofan.inl c = BinaryCofan.inl (cofans X' Y') ≫ f →
      αY ≫ BinaryCofan.inr c = BinaryCofan.inr (cofans X' Y') ≫ f →
        IsPullback (BinaryCofan.inl (cofans X' Y')) αX f (BinaryCofan.inl c) ∧
          IsPullback (BinaryCofan.inr (cofans X' Y')) αY f (BinaryCofan.inr c)
h₂ :
  {Z : C} →
    (f : Z ⟶ c.pt) →
      IsColimit
        (BinaryCofan.mk (PullbackCone.fst (cones f (BinaryCofan.inl c)))
          (PullbackCone.fst (cones f (BinaryCofan.inr c))))
X' Y' : C
c' : BinaryCofan X' Y'
αX : X' ⟶ X
αY : Y' ⟶ Y
f : c'.pt ⟶ c.pt
hX : αX ≫ BinaryCofan.inl c = BinaryCofan.inl c' ≫ f
hY : αY ≫ BinaryCofan.inr c = BinaryCofan.inr c' ≫ f
h : IsColimit c'
e : c'.pt ≅ (cofans X' Y').pt := IsColimit.coconePointUniqueUpToIso h (colimits X' Y')
hl : IsPullback (BinaryCofan.inl (cofans X' Y')) αX (e.inv ≫ f) (BinaryCofan.inl c)
hr : IsPullback (BinaryCofan.inr (cofans X' Y')) αY (e.inv ≫ f) (BinaryCofan.inr c)
this✝ : IsIso (𝟙 Y')
this : BinaryCofan.inr c' ≫ e.hom = 𝟙 Y' ≫ BinaryCofan.inr (cofans X' Y')
⊢ IsPullback (BinaryCofan.inr c') (𝟙 Y' ≫ αY) (e.hom ≫ e.inv ≫ f) (BinaryCofan.inr c)
case mp.intro.intro.right
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
X✝ Y✝ X Y : C
c : BinaryCofan X Y
cofans : (X Y : C) → BinaryCofan X Y
colimits : (X Y : C) → IsColimit (cofans X Y)
cones : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → PullbackCone f g
limits : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → IsLimit (cones f g)
h₁ :
  ∀ {X' Y' : C} (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : (cofans X' Y').pt ⟶ c.pt),
    αX ≫ BinaryCofan.inl c = BinaryCofan.inl (cofans X' Y') ≫ f →
      αY ≫ BinaryCofan.inr c = BinaryCofan.inr (cofans X' Y') ≫ f →
        IsPullback (BinaryCofan.inl (cofans X' Y')) αX f (BinaryCofan.inl c) ∧
          IsPullback (BinaryCofan.inr (cofans X' Y')) αY f (BinaryCofan.inr c)
h₂ :
  {Z : C} →
    (f : Z ⟶ c.pt) →
      IsColimit
        (BinaryCofan.mk (PullbackCone.fst (cones f (BinaryCofan.inl c)))
          (PullbackCone.fst (cones f (BinaryCofan.inr c))))
X' Y' : C
c' : BinaryCofan X' Y'
αX : X' ⟶ X
αY : Y' ⟶ Y
f : c'.pt ⟶ c.pt
hX : αX ≫ BinaryCofan.inl c = BinaryCofan.inl c' ≫ f
hY : αY ≫ BinaryCofan.inr c = BinaryCofan.inr c' ≫ f
h : IsColimit c'
e : c'.pt ≅ (cofans X' Y').pt := IsColimit.coconePointUniqueUpToIso h (colimits X' Y')
hl : IsPullback (BinaryCofan.inl (cofans X' Y')) αX (e.inv ≫ f) (BinaryCofan.inl c)
hr : IsPullback (BinaryCofan.inr (cofans X' Y')) αY (e.inv ≫ f) (BinaryCofan.inr c)
this : IsIso (𝟙 Y')
⊢ IsPullback (BinaryCofan.inr c') (𝟙 Y' ≫ αY) (e.hom ≫ e.inv ≫ f) (BinaryCofan.inr c)
have : c'.inr ≫ e.hom = 𝟙 Y' ≫ (cofans X' Y').inr := by
  dsimp
  simp
no goals
case mp.intro.intro.right
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
X✝ Y✝ X Y : C
c : BinaryCofan X Y
cofans : (X Y : C) → BinaryCofan X Y
colimits : (X Y : C) → IsColimit (cofans X Y)
cones : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → PullbackCone f g
limits : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → IsLimit (cones f g)
h₁ :
  ∀ {X' Y' : C} (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : (cofans X' Y').pt ⟶ c.pt),
    αX ≫ BinaryCofan.inl c = BinaryCofan.inl (cofans X' Y') ≫ f →
      αY ≫ BinaryCofan.inr c = BinaryCofan.inr (cofans X' Y') ≫ f →
        IsPullback (BinaryCofan.inl (cofans X' Y')) αX f (BinaryCofan.inl c) ∧
          IsPullback (BinaryCofan.inr (cofans X' Y')) αY f (BinaryCofan.inr c)
h₂ :
  {Z : C} →
    (f : Z ⟶ c.pt) →
      IsColimit
        (BinaryCofan.mk (PullbackCone.fst (cones f (BinaryCofan.inl c)))
          (PullbackCone.fst (cones f (BinaryCofan.inr c))))
X' Y' : C
c' : BinaryCofan X' Y'
αX : X' ⟶ X
αY : Y' ⟶ Y
f : c'.pt ⟶ c.pt
hX : αX ≫ BinaryCofan.inl c = BinaryCofan.inl c' ≫ f
hY : αY ≫ BinaryCofan.inr c = BinaryCofan.inr c' ≫ f
h : IsColimit c'
e : c'.pt ≅ (cofans X' Y').pt := IsColimit.coconePointUniqueUpToIso h (colimits X' Y')
hl : IsPullback (BinaryCofan.inl (cofans X' Y')) αX (e.inv ≫ f) (BinaryCofan.inl c)
hr : IsPullback (BinaryCofan.inr (cofans X' Y')) αY (e.inv ≫ f) (BinaryCofan.inr c)
this✝ : IsIso (𝟙 Y')
this : BinaryCofan.inr c' ≫ e.hom = 𝟙 Y' ≫ BinaryCofan.inr (cofans X' Y')
⊢ IsPullback (BinaryCofan.inr c') (𝟙 Y' ≫ αY) (e.hom ≫ e.inv ≫ f) (BinaryCofan.inr c)
exact (IsPullback.of_vert_isIso ⟨this⟩).paste_vert hr
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
X✝ Y✝ X Y : C
c : BinaryCofan X Y
cofans : (X Y : C) → BinaryCofan X Y
colimits : (X Y : C) → IsColimit (cofans X Y)
cones : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → PullbackCone f g
limits : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → IsLimit (cones f g)
h₁ :
  ∀ {X' Y' : C} (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : (cofans X' Y').pt ⟶ c.pt),
    αX ≫ BinaryCofan.inl c = BinaryCofan.inl (cofans X' Y') ≫ f →
      αY ≫ BinaryCofan.inr c = BinaryCofan.inr (cofans X' Y') ≫ f →
        IsPullback (BinaryCofan.inl (cofans X' Y')) αX f (BinaryCofan.inl c) ∧
          IsPullback (BinaryCofan.inr (cofans X' Y')) αY f (BinaryCofan.inr c)
h₂ :
  {Z : C} →
    (f : Z ⟶ c.pt) →
      IsColimit
        (BinaryCofan.mk (PullbackCone.fst (cones f (BinaryCofan.inl c)))
          (PullbackCone.fst (cones f (BinaryCofan.inr c))))
X' Y' : C
c' : BinaryCofan X' Y'
αX : X' ⟶ X
αY : Y' ⟶ Y
f : c'.pt ⟶ c.pt
hX : αX ≫ BinaryCofan.inl c = BinaryCofan.inl c' ≫ f
hY : αY ≫ BinaryCofan.inr c = BinaryCofan.inr c' ≫ f
h : IsColimit c'
e : c'.pt ≅ (cofans X' Y').pt := IsColimit.coconePointUniqueUpToIso h (colimits X' Y')
hl : IsPullback (BinaryCofan.inl (cofans X' Y')) αX (e.inv ≫ f) (BinaryCofan.inl c)
hr : IsPullback (BinaryCofan.inr (cofans X' Y')) αY (e.inv ≫ f) (BinaryCofan.inr c)
this : IsIso (𝟙 Y')
⊢ BinaryCofan.inr c' ≫ (IsColimit.coconePointUniqueUpToIso h (colimits X' Y')).hom =
    𝟙 Y' ≫ BinaryCofan.inr (cofans X' Y')
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
X✝ Y✝ X Y : C
c : BinaryCofan X Y
cofans : (X Y : C) → BinaryCofan X Y
colimits : (X Y : C) → IsColimit (cofans X Y)
cones : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → PullbackCone f g
limits : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → IsLimit (cones f g)
h₁ :
  ∀ {X' Y' : C} (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : (cofans X' Y').pt ⟶ c.pt),
    αX ≫ BinaryCofan.inl c = BinaryCofan.inl (cofans X' Y') ≫ f →
      αY ≫ BinaryCofan.inr c = BinaryCofan.inr (cofans X' Y') ≫ f →
        IsPullback (BinaryCofan.inl (cofans X' Y')) αX f (BinaryCofan.inl c) ∧
          IsPullback (BinaryCofan.inr (cofans X' Y')) αY f (BinaryCofan.inr c)
h₂ :
  {Z : C} →
    (f : Z ⟶ c.pt) →
      IsColimit
        (BinaryCofan.mk (PullbackCone.fst (cones f (BinaryCofan.inl c)))
          (PullbackCone.fst (cones f (BinaryCofan.inr c))))
X' Y' : C
c' : BinaryCofan X' Y'
αX : X' ⟶ X
αY : Y' ⟶ Y
f : c'.pt ⟶ c.pt
hX : αX ≫ BinaryCofan.inl c = BinaryCofan.inl c' ≫ f
hY : αY ≫ BinaryCofan.inr c = BinaryCofan.inr c' ≫ f
h : IsColimit c'
e : c'.pt ≅ (cofans X' Y').pt := IsColimit.coconePointUniqueUpToIso h (colimits X' Y')
hl : IsPullback (BinaryCofan.inl (cofans X' Y')) αX (e.inv ≫ f) (BinaryCofan.inl c)
hr : IsPullback (BinaryCofan.inr (cofans X' Y')) αY (e.inv ≫ f) (BinaryCofan.inr c)
this : IsIso (𝟙 Y')
⊢ BinaryCofan.inr c' ≫ e.hom = 𝟙 Y' ≫ BinaryCofan.inr (cofans X' Y')
dsimp
no goals
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
X✝ Y✝ X Y : C
c : BinaryCofan X Y
cofans : (X Y : C) → BinaryCofan X Y
colimits : (X Y : C) → IsColimit (cofans X Y)
cones : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → PullbackCone f g
limits : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → IsLimit (cones f g)
h₁ :
  ∀ {X' Y' : C} (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : (cofans X' Y').pt ⟶ c.pt),
    αX ≫ BinaryCofan.inl c = BinaryCofan.inl (cofans X' Y') ≫ f →
      αY ≫ BinaryCofan.inr c = BinaryCofan.inr (cofans X' Y') ≫ f →
        IsPullback (BinaryCofan.inl (cofans X' Y')) αX f (BinaryCofan.inl c) ∧
          IsPullback (BinaryCofan.inr (cofans X' Y')) αY f (BinaryCofan.inr c)
h₂ :
  {Z : C} →
    (f : Z ⟶ c.pt) →
      IsColimit
        (BinaryCofan.mk (PullbackCone.fst (cones f (BinaryCofan.inl c)))
          (PullbackCone.fst (cones f (BinaryCofan.inr c))))
X' Y' : C
c' : BinaryCofan X' Y'
αX : X' ⟶ X
αY : Y' ⟶ Y
f : c'.pt ⟶ c.pt
hX : αX ≫ BinaryCofan.inl c = BinaryCofan.inl c' ≫ f
hY : αY ≫ BinaryCofan.inr c = BinaryCofan.inr c' ≫ f
h : IsColimit c'
e : c'.pt ≅ (cofans X' Y').pt := IsColimit.coconePointUniqueUpToIso h (colimits X' Y')
hl : IsPullback (BinaryCofan.inl (cofans X' Y')) αX (e.inv ≫ f) (BinaryCofan.inl c)
hr : IsPullback (BinaryCofan.inr (cofans X' Y')) αY (e.inv ≫ f) (BinaryCofan.inr c)
this : IsIso (𝟙 Y')
⊢ BinaryCofan.inr c' ≫ (IsColimit.coconePointUniqueUpToIso h (colimits X' Y')).hom =
    𝟙 Y' ≫ BinaryCofan.inr (cofans X' Y')
simp
case mpr.intro
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
X✝ Y✝ X Y : C
c : BinaryCofan X Y
cofans : (X Y : C) → BinaryCofan X Y
colimits : (X Y : C) → IsColimit (cofans X Y)
cones : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → PullbackCone f g
limits : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → IsLimit (cones f g)
h₁ :
  ∀ {X' Y' : C} (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : (cofans X' Y').pt ⟶ c.pt),
    αX ≫ BinaryCofan.inl c = BinaryCofan.inl (cofans X' Y') ≫ f →
      αY ≫ BinaryCofan.inr c = BinaryCofan.inr (cofans X' Y') ≫ f →
        IsPullback (BinaryCofan.inl (cofans X' Y')) αX f (BinaryCofan.inl c) ∧
          IsPullback (BinaryCofan.inr (cofans X' Y')) αY f (BinaryCofan.inr c)
h₂ :
  {Z : C} →
    (f : Z ⟶ c.pt) →
      IsColimit
        (BinaryCofan.mk (PullbackCone.fst (cones f (BinaryCofan.inl c)))
          (PullbackCone.fst (cones f (BinaryCofan.inr c))))
X' Y' : C
c' : BinaryCofan X' Y'
αX : X' ⟶ X
αY : Y' ⟶ Y
f : c'.pt ⟶ c.pt
hX : αX ≫ BinaryCofan.inl c = BinaryCofan.inl c' ≫ f
hY : αY ≫ BinaryCofan.inr c = BinaryCofan.inr c' ≫ f
H₁ : IsPullback (BinaryCofan.inl c') αX f (BinaryCofan.inl c)
H₂ : IsPullback (BinaryCofan.inr c') αY f (BinaryCofan.inr c)
⊢ Nonempty (IsColimit c')
case mpr
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
X✝ Y✝ X Y : C
c : BinaryCofan X Y
cofans : (X Y : C) → BinaryCofan X Y
colimits : (X Y : C) → IsColimit (cofans X Y)
cones : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → PullbackCone f g
limits : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → IsLimit (cones f g)
h₁ :
  ∀ {X' Y' : C} (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : (cofans X' Y').pt ⟶ c.pt),
    αX ≫ BinaryCofan.inl c = BinaryCofan.inl (cofans X' Y') ≫ f →
      αY ≫ BinaryCofan.inr c = BinaryCofan.inr (cofans X' Y') ≫ f →
        IsPullback (BinaryCofan.inl (cofans X' Y')) αX f (BinaryCofan.inl c) ∧
          IsPullback (BinaryCofan.inr (cofans X' Y')) αY f (BinaryCofan.inr c)
h₂ :
  {Z : C} →
    (f : Z ⟶ c.pt) →
      IsColimit
        (BinaryCofan.mk (PullbackCone.fst (cones f (BinaryCofan.inl c)))
          (PullbackCone.fst (cones f (BinaryCofan.inr c))))
X' Y' : C
c' : BinaryCofan X' Y'
αX : X' ⟶ X
αY : Y' ⟶ Y
f : c'.pt ⟶ c.pt
hX : αX ≫ BinaryCofan.inl c = BinaryCofan.inl c' ≫ f
hY : αY ≫ BinaryCofan.inr c = BinaryCofan.inr c' ≫ f
⊢ IsPullback (BinaryCofan.inl c') αX f (BinaryCofan.inl c) ∧ IsPullback (BinaryCofan.inr c') αY f (BinaryCofan.inr c) →
    Nonempty (IsColimit c')
rintro ⟨H₁, H₂⟩
case mpr.intro
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
X✝ Y✝ X Y : C
c : BinaryCofan X Y
cofans : (X Y : C) → BinaryCofan X Y
colimits : (X Y : C) → IsColimit (cofans X Y)
cones : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → PullbackCone f g
limits : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → IsLimit (cones f g)
h₁ :
  ∀ {X' Y' : C} (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : (cofans X' Y').pt ⟶ c.pt),
    αX ≫ BinaryCofan.inl c = BinaryCofan.inl (cofans X' Y') ≫ f →
      αY ≫ BinaryCofan.inr c = BinaryCofan.inr (cofans X' Y') ≫ f →
        IsPullback (BinaryCofan.inl (cofans X' Y')) αX f (BinaryCofan.inl c) ∧
          IsPullback (BinaryCofan.inr (cofans X' Y')) αY f (BinaryCofan.inr c)
h₂ :
  {Z : C} →
    (f : Z ⟶ c.pt) →
      IsColimit
        (BinaryCofan.mk (PullbackCone.fst (cones f (BinaryCofan.inl c)))
          (PullbackCone.fst (cones f (BinaryCofan.inr c))))
X' Y' : C
c' : BinaryCofan X' Y'
αX : X' ⟶ X
αY : Y' ⟶ Y
f : c'.pt ⟶ c.pt
hX : αX ≫ BinaryCofan.inl c = BinaryCofan.inl c' ≫ f
hY : αY ≫ BinaryCofan.inr c = BinaryCofan.inr c' ≫ f
H₁ : IsPullback (BinaryCofan.inl c') αX f (BinaryCofan.inl c)
H₂ : IsPullback (BinaryCofan.inr c') αY f (BinaryCofan.inr c)
⊢ IsColimit (BinaryCofan.mk (BinaryCofan.inl c') (BinaryCofan.inr c'))
case mpr.intro
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
X✝ Y✝ X Y : C
c : BinaryCofan X Y
cofans : (X Y : C) → BinaryCofan X Y
colimits : (X Y : C) → IsColimit (cofans X Y)
cones : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → PullbackCone f g
limits : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → IsLimit (cones f g)
h₁ :
  ∀ {X' Y' : C} (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : (cofans X' Y').pt ⟶ c.pt),
    αX ≫ BinaryCofan.inl c = BinaryCofan.inl (cofans X' Y') ≫ f →
      αY ≫ BinaryCofan.inr c = BinaryCofan.inr (cofans X' Y') ≫ f →
        IsPullback (BinaryCofan.inl (cofans X' Y')) αX f (BinaryCofan.inl c) ∧
          IsPullback (BinaryCofan.inr (cofans X' Y')) αY f (BinaryCofan.inr c)
h₂ :
  {Z : C} →
    (f : Z ⟶ c.pt) →
      IsColimit
        (BinaryCofan.mk (PullbackCone.fst (cones f (BinaryCofan.inl c)))
          (PullbackCone.fst (cones f (BinaryCofan.inr c))))
X' Y' : C
c' : BinaryCofan X' Y'
αX : X' ⟶ X
αY : Y' ⟶ Y
f : c'.pt ⟶ c.pt
hX : αX ≫ BinaryCofan.inl c = BinaryCofan.inl c' ≫ f
hY : αY ≫ BinaryCofan.inr c = BinaryCofan.inr c' ≫ f
H₁ : IsPullback (BinaryCofan.inl c') αX f (BinaryCofan.inl c)
H₂ : IsPullback (BinaryCofan.inr c') αY f (BinaryCofan.inr c)
⊢ Nonempty (IsColimit c')
refine' ⟨IsColimit.ofIsoColimit _ <| (isoBinaryCofanMk _).symm⟩
case mpr.intro
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
X✝ Y✝ X Y : C
c : BinaryCofan X Y
cofans : (X Y : C) → BinaryCofan X Y
colimits : (X Y : C) → IsColimit (cofans X Y)
cones : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → PullbackCone f g
limits : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → IsLimit (cones f g)
h₁ :
  ∀ {X' Y' : C} (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : (cofans X' Y').pt ⟶ c.pt),
    αX ≫ BinaryCofan.inl c = BinaryCofan.inl (cofans X' Y') ≫ f →
      αY ≫ BinaryCofan.inr c = BinaryCofan.inr (cofans X' Y') ≫ f →
        IsPullback (BinaryCofan.inl (cofans X' Y')) αX f (BinaryCofan.inl c) ∧
          IsPullback (BinaryCofan.inr (cofans X' Y')) αY f (BinaryCofan.inr c)
h₂ :
  {Z : C} →
    (f : Z ⟶ c.pt) →
      IsColimit
        (BinaryCofan.mk (PullbackCone.fst (cones f (BinaryCofan.inl c)))
          (PullbackCone.fst (cones f (BinaryCofan.inr c))))
X' Y' : C
c' : BinaryCofan X' Y'
αX : X' ⟶ X
αY : Y' ⟶ Y
f : c'.pt ⟶ c.pt
hX : αX ≫ BinaryCofan.inl c = BinaryCofan.inl c' ≫ f
hY : αY ≫ BinaryCofan.inr c = BinaryCofan.inr c' ≫ f
H₁ : IsPullback (BinaryCofan.inl c') αX f (BinaryCofan.inl c)
H₂ : IsPullback (BinaryCofan.inr c') αY f (BinaryCofan.inr c)
e₁ : X' ≅ (cones f (BinaryCofan.inl c)).pt :=
  IsLimit.conePointUniqueUpToIso (IsPullback.isLimit H₁) (limits f (BinaryCofan.inl c))
⊢ IsColimit (BinaryCofan.mk (BinaryCofan.inl c') (BinaryCofan.inr c'))
case mpr.intro
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
X✝ Y✝ X Y : C
c : BinaryCofan X Y
cofans : (X Y : C) → BinaryCofan X Y
colimits : (X Y : C) → IsColimit (cofans X Y)
cones : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → PullbackCone f g
limits : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → IsLimit (cones f g)
h₁ :
  ∀ {X' Y' : C} (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : (cofans X' Y').pt ⟶ c.pt),
    αX ≫ BinaryCofan.inl c = BinaryCofan.inl (cofans X' Y') ≫ f →
      αY ≫ BinaryCofan.inr c = BinaryCofan.inr (cofans X' Y') ≫ f →
        IsPullback (BinaryCofan.inl (cofans X' Y')) αX f (BinaryCofan.inl c) ∧
          IsPullback (BinaryCofan.inr (cofans X' Y')) αY f (BinaryCofan.inr c)
h₂ :
  {Z : C} →
    (f : Z ⟶ c.pt) →
      IsColimit
        (BinaryCofan.mk (PullbackCone.fst (cones f (BinaryCofan.inl c)))
          (PullbackCone.fst (cones f (BinaryCofan.inr c))))
X' Y' : C
c' : BinaryCofan X' Y'
αX : X' ⟶ X
αY : Y' ⟶ Y
f : c'.pt ⟶ c.pt
hX : αX ≫ BinaryCofan.inl c = BinaryCofan.inl c' ≫ f
hY : αY ≫ BinaryCofan.inr c = BinaryCofan.inr c' ≫ f
H₁ : IsPullback (BinaryCofan.inl c') αX f (BinaryCofan.inl c)
H₂ : IsPullback (BinaryCofan.inr c') αY f (BinaryCofan.inr c)
⊢ IsColimit (BinaryCofan.mk (BinaryCofan.inl c') (BinaryCofan.inr c'))
let e₁ : X' ≅ _ := H₁.isLimit.conePointUniqueUpToIso (limits _ _)
case mpr.intro
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
X✝ Y✝ X Y : C
c : BinaryCofan X Y
cofans : (X Y : C) → BinaryCofan X Y
colimits : (X Y : C) → IsColimit (cofans X Y)
cones : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → PullbackCone f g
limits : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → IsLimit (cones f g)
h₁ :
  ∀ {X' Y' : C} (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : (cofans X' Y').pt ⟶ c.pt),
    αX ≫ BinaryCofan.inl c = BinaryCofan.inl (cofans X' Y') ≫ f →
      αY ≫ BinaryCofan.inr c = BinaryCofan.inr (cofans X' Y') ≫ f →
        IsPullback (BinaryCofan.inl (cofans X' Y')) αX f (BinaryCofan.inl c) ∧
          IsPullback (BinaryCofan.inr (cofans X' Y')) αY f (BinaryCofan.inr c)
h₂ :
  {Z : C} →
    (f : Z ⟶ c.pt) →
      IsColimit
        (BinaryCofan.mk (PullbackCone.fst (cones f (BinaryCofan.inl c)))
          (PullbackCone.fst (cones f (BinaryCofan.inr c))))
X' Y' : C
c' : BinaryCofan X' Y'
αX : X' ⟶ X
αY : Y' ⟶ Y
f : c'.pt ⟶ c.pt
hX : αX ≫ BinaryCofan.inl c = BinaryCofan.inl c' ≫ f
hY : αY ≫ BinaryCofan.inr c = BinaryCofan.inr c' ≫ f
H₁ : IsPullback (BinaryCofan.inl c') αX f (BinaryCofan.inl c)
H₂ : IsPullback (BinaryCofan.inr c') αY f (BinaryCofan.inr c)
e₁ : X' ≅ (cones f (BinaryCofan.inl c)).pt :=
  IsLimit.conePointUniqueUpToIso (IsPullback.isLimit H₁) (limits f (BinaryCofan.inl c))
e₂ : Y' ≅ (cones f (BinaryCofan.inr c)).pt :=
  IsLimit.conePointUniqueUpToIso (IsPullback.isLimit H₂) (limits f (BinaryCofan.inr c))
⊢ IsColimit (BinaryCofan.mk (BinaryCofan.inl c') (BinaryCofan.inr c'))
case mpr.intro
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
X✝ Y✝ X Y : C
c : BinaryCofan X Y
cofans : (X Y : C) → BinaryCofan X Y
colimits : (X Y : C) → IsColimit (cofans X Y)
cones : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → PullbackCone f g
limits : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → IsLimit (cones f g)
h₁ :
  ∀ {X' Y' : C} (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : (cofans X' Y').pt ⟶ c.pt),
    αX ≫ BinaryCofan.inl c = BinaryCofan.inl (cofans X' Y') ≫ f →
      αY ≫ BinaryCofan.inr c = BinaryCofan.inr (cofans X' Y') ≫ f →
        IsPullback (BinaryCofan.inl (cofans X' Y')) αX f (BinaryCofan.inl c) ∧
          IsPullback (BinaryCofan.inr (cofans X' Y')) αY f (BinaryCofan.inr c)
h₂ :
  {Z : C} →
    (f : Z ⟶ c.pt) →
      IsColimit
        (BinaryCofan.mk (PullbackCone.fst (cones f (BinaryCofan.inl c)))
          (PullbackCone.fst (cones f (BinaryCofan.inr c))))
X' Y' : C
c' : BinaryCofan X' Y'
αX : X' ⟶ X
αY : Y' ⟶ Y
f : c'.pt ⟶ c.pt
hX : αX ≫ BinaryCofan.inl c = BinaryCofan.inl c' ≫ f
hY : αY ≫ BinaryCofan.inr c = BinaryCofan.inr c' ≫ f
H₁ : IsPullback (BinaryCofan.inl c') αX f (BinaryCofan.inl c)
H₂ : IsPullback (BinaryCofan.inr c') αY f (BinaryCofan.inr c)
e₁ : X' ≅ (cones f (BinaryCofan.inl c)).pt :=
  IsLimit.conePointUniqueUpToIso (IsPullback.isLimit H₁) (limits f (BinaryCofan.inl c))
⊢ IsColimit (BinaryCofan.mk (BinaryCofan.inl c') (BinaryCofan.inr c'))
let e₂ : Y' ≅ _ := H₂.isLimit.conePointUniqueUpToIso (limits _ _)
case mpr.intro
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
X✝ Y✝ X Y : C
c : BinaryCofan X Y
cofans : (X Y : C) → BinaryCofan X Y
colimits : (X Y : C) → IsColimit (cofans X Y)
cones : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → PullbackCone f g
limits : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → IsLimit (cones f g)
h₁ :
  ∀ {X' Y' : C} (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : (cofans X' Y').pt ⟶ c.pt),
    αX ≫ BinaryCofan.inl c = BinaryCofan.inl (cofans X' Y') ≫ f →
      αY ≫ BinaryCofan.inr c = BinaryCofan.inr (cofans X' Y') ≫ f →
        IsPullback (BinaryCofan.inl (cofans X' Y')) αX f (BinaryCofan.inl c) ∧
          IsPullback (BinaryCofan.inr (cofans X' Y')) αY f (BinaryCofan.inr c)
h₂ :
  {Z : C} →
    (f : Z ⟶ c.pt) →
      IsColimit
        (BinaryCofan.mk (PullbackCone.fst (cones f (BinaryCofan.inl c)))
          (PullbackCone.fst (cones f (BinaryCofan.inr c))))
X' Y' : C
c' : BinaryCofan X' Y'
αX : X' ⟶ X
αY : Y' ⟶ Y
f : c'.pt ⟶ c.pt
hX : αX ≫ BinaryCofan.inl c = BinaryCofan.inl c' ≫ f
hY : αY ≫ BinaryCofan.inr c = BinaryCofan.inr c' ≫ f
H₁ : IsPullback (BinaryCofan.inl c') αX f (BinaryCofan.inl c)
H₂ : IsPullback (BinaryCofan.inr c') αY f (BinaryCofan.inr c)
e₁ : X' ≅ (cones f (BinaryCofan.inl c)).pt :=
  IsLimit.conePointUniqueUpToIso (IsPullback.isLimit H₁) (limits f (BinaryCofan.inl c))
e₂ : Y' ≅ (cones f (BinaryCofan.inr c)).pt :=
  IsLimit.conePointUniqueUpToIso (IsPullback.isLimit H₂) (limits f (BinaryCofan.inr c))
he₁ : BinaryCofan.inl c' = e₁.hom ≫ PullbackCone.fst (cones f (BinaryCofan.inl c))
⊢ IsColimit (BinaryCofan.mk (BinaryCofan.inl c') (BinaryCofan.inr c'))
case mpr.intro
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
X✝ Y✝ X Y : C
c : BinaryCofan X Y
cofans : (X Y : C) → BinaryCofan X Y
colimits : (X Y : C) → IsColimit (cofans X Y)
cones : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → PullbackCone f g
limits : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → IsLimit (cones f g)
h₁ :
  ∀ {X' Y' : C} (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : (cofans X' Y').pt ⟶ c.pt),
    αX ≫ BinaryCofan.inl c = BinaryCofan.inl (cofans X' Y') ≫ f →
      αY ≫ BinaryCofan.inr c = BinaryCofan.inr (cofans X' Y') ≫ f →
        IsPullback (BinaryCofan.inl (cofans X' Y')) αX f (BinaryCofan.inl c) ∧
          IsPullback (BinaryCofan.inr (cofans X' Y')) αY f (BinaryCofan.inr c)
h₂ :
  {Z : C} →
    (f : Z ⟶ c.pt) →
      IsColimit
        (BinaryCofan.mk (PullbackCone.fst (cones f (BinaryCofan.inl c)))
          (PullbackCone.fst (cones f (BinaryCofan.inr c))))
X' Y' : C
c' : BinaryCofan X' Y'
αX : X' ⟶ X
αY : Y' ⟶ Y
f : c'.pt ⟶ c.pt
hX : αX ≫ BinaryCofan.inl c = BinaryCofan.inl c' ≫ f
hY : αY ≫ BinaryCofan.inr c = BinaryCofan.inr c' ≫ f
H₁ : IsPullback (BinaryCofan.inl c') αX f (BinaryCofan.inl c)
H₂ : IsPullback (BinaryCofan.inr c') αY f (BinaryCofan.inr c)
e₁ : X' ≅ (cones f (BinaryCofan.inl c)).pt :=
  IsLimit.conePointUniqueUpToIso (IsPullback.isLimit H₁) (limits f (BinaryCofan.inl c))
e₂ : Y' ≅ (cones f (BinaryCofan.inr c)).pt :=
  IsLimit.conePointUniqueUpToIso (IsPullback.isLimit H₂) (limits f (BinaryCofan.inr c))
⊢ IsColimit (BinaryCofan.mk (BinaryCofan.inl c') (BinaryCofan.inr c'))
have he₁ : c'.inl = e₁.hom ≫ (cones f c.inl).fst := by simp
case mpr.intro
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
X✝ Y✝ X Y : C
c : BinaryCofan X Y
cofans : (X Y : C) → BinaryCofan X Y
colimits : (X Y : C) → IsColimit (cofans X Y)
cones : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → PullbackCone f g
limits : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → IsLimit (cones f g)
h₁ :
  ∀ {X' Y' : C} (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : (cofans X' Y').pt ⟶ c.pt),
    αX ≫ BinaryCofan.inl c = BinaryCofan.inl (cofans X' Y') ≫ f →
      αY ≫ BinaryCofan.inr c = BinaryCofan.inr (cofans X' Y') ≫ f →
        IsPullback (BinaryCofan.inl (cofans X' Y')) αX f (BinaryCofan.inl c) ∧
          IsPullback (BinaryCofan.inr (cofans X' Y')) αY f (BinaryCofan.inr c)
h₂ :
  {Z : C} →
    (f : Z ⟶ c.pt) →
      IsColimit
        (BinaryCofan.mk (PullbackCone.fst (cones f (BinaryCofan.inl c)))
          (PullbackCone.fst (cones f (BinaryCofan.inr c))))
X' Y' : C
c' : BinaryCofan X' Y'
αX : X' ⟶ X
αY : Y' ⟶ Y
f : c'.pt ⟶ c.pt
hX : αX ≫ BinaryCofan.inl c = BinaryCofan.inl c' ≫ f
hY : αY ≫ BinaryCofan.inr c = BinaryCofan.inr c' ≫ f
H₁ : IsPullback (BinaryCofan.inl c') αX f (BinaryCofan.inl c)
H₂ : IsPullback (BinaryCofan.inr c') αY f (BinaryCofan.inr c)
e₁ : X' ≅ (cones f (BinaryCofan.inl c)).pt :=
  IsLimit.conePointUniqueUpToIso (IsPullback.isLimit H₁) (limits f (BinaryCofan.inl c))
e₂ : Y' ≅ (cones f (BinaryCofan.inr c)).pt :=
  IsLimit.conePointUniqueUpToIso (IsPullback.isLimit H₂) (limits f (BinaryCofan.inr c))
he₁ : BinaryCofan.inl c' = e₁.hom ≫ PullbackCone.fst (cones f (BinaryCofan.inl c))
he₂ : BinaryCofan.inr c' = e₂.hom ≫ PullbackCone.fst (cones f (BinaryCofan.inr c))
⊢ IsColimit (BinaryCofan.mk (BinaryCofan.inl c') (BinaryCofan.inr c'))
case mpr.intro
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
X✝ Y✝ X Y : C
c : BinaryCofan X Y
cofans : (X Y : C) → BinaryCofan X Y
colimits : (X Y : C) → IsColimit (cofans X Y)
cones : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → PullbackCone f g
limits : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → IsLimit (cones f g)
h₁ :
  ∀ {X' Y' : C} (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : (cofans X' Y').pt ⟶ c.pt),
    αX ≫ BinaryCofan.inl c = BinaryCofan.inl (cofans X' Y') ≫ f →
      αY ≫ BinaryCofan.inr c = BinaryCofan.inr (cofans X' Y') ≫ f →
        IsPullback (BinaryCofan.inl (cofans X' Y')) αX f (BinaryCofan.inl c) ∧
          IsPullback (BinaryCofan.inr (cofans X' Y')) αY f (BinaryCofan.inr c)
h₂ :
  {Z : C} →
    (f : Z ⟶ c.pt) →
      IsColimit
        (BinaryCofan.mk (PullbackCone.fst (cones f (BinaryCofan.inl c)))
          (PullbackCone.fst (cones f (BinaryCofan.inr c))))
X' Y' : C
c' : BinaryCofan X' Y'
αX : X' ⟶ X
αY : Y' ⟶ Y
f : c'.pt ⟶ c.pt
hX : αX ≫ BinaryCofan.inl c = BinaryCofan.inl c' ≫ f
hY : αY ≫ BinaryCofan.inr c = BinaryCofan.inr c' ≫ f
H₁ : IsPullback (BinaryCofan.inl c') αX f (BinaryCofan.inl c)
H₂ : IsPullback (BinaryCofan.inr c') αY f (BinaryCofan.inr c)
e₁ : X' ≅ (cones f (BinaryCofan.inl c)).pt :=
  IsLimit.conePointUniqueUpToIso (IsPullback.isLimit H₁) (limits f (BinaryCofan.inl c))
e₂ : Y' ≅ (cones f (BinaryCofan.inr c)).pt :=
  IsLimit.conePointUniqueUpToIso (IsPullback.isLimit H₂) (limits f (BinaryCofan.inr c))
he₁ : BinaryCofan.inl c' = e₁.hom ≫ PullbackCone.fst (cones f (BinaryCofan.inl c))
⊢ IsColimit (BinaryCofan.mk (BinaryCofan.inl c') (BinaryCofan.inr c'))
have he₂ : c'.inr = e₂.hom ≫ (cones f c.inr).fst := by simp
case mpr.intro
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
X✝ Y✝ X Y : C
c : BinaryCofan X Y
cofans : (X Y : C) → BinaryCofan X Y
colimits : (X Y : C) → IsColimit (cofans X Y)
cones : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → PullbackCone f g
limits : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → IsLimit (cones f g)
h₁ :
  ∀ {X' Y' : C} (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : (cofans X' Y').pt ⟶ c.pt),
    αX ≫ BinaryCofan.inl c = BinaryCofan.inl (cofans X' Y') ≫ f →
      αY ≫ BinaryCofan.inr c = BinaryCofan.inr (cofans X' Y') ≫ f →
        IsPullback (BinaryCofan.inl (cofans X' Y')) αX f (BinaryCofan.inl c) ∧
          IsPullback (BinaryCofan.inr (cofans X' Y')) αY f (BinaryCofan.inr c)
h₂ :
  {Z : C} →
    (f : Z ⟶ c.pt) →
      IsColimit
        (BinaryCofan.mk (PullbackCone.fst (cones f (BinaryCofan.inl c)))
          (PullbackCone.fst (cones f (BinaryCofan.inr c))))
X' Y' : C
c' : BinaryCofan X' Y'
αX : X' ⟶ X
αY : Y' ⟶ Y
f : c'.pt ⟶ c.pt
hX : αX ≫ BinaryCofan.inl c = BinaryCofan.inl c' ≫ f
hY : αY ≫ BinaryCofan.inr c = BinaryCofan.inr c' ≫ f
H₁ : IsPullback (BinaryCofan.inl c') αX f (BinaryCofan.inl c)
H₂ : IsPullback (BinaryCofan.inr c') αY f (BinaryCofan.inr c)
e₁ : X' ≅ (cones f (BinaryCofan.inl c)).pt :=
  IsLimit.conePointUniqueUpToIso (IsPullback.isLimit H₁) (limits f (BinaryCofan.inl c))
e₂ : Y' ≅ (cones f (BinaryCofan.inr c)).pt :=
  IsLimit.conePointUniqueUpToIso (IsPullback.isLimit H₂) (limits f (BinaryCofan.inr c))
he₁ : BinaryCofan.inl c' = e₁.hom ≫ PullbackCone.fst (cones f (BinaryCofan.inl c))
he₂ : BinaryCofan.inr c' = e₂.hom ≫ PullbackCone.fst (cones f (BinaryCofan.inr c))
⊢ IsColimit
    (BinaryCofan.mk (e₁.hom ≫ PullbackCone.fst (cones f (BinaryCofan.inl c)))
      (e₂.hom ≫ PullbackCone.fst (cones f (BinaryCofan.inr c))))
case mpr.intro
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
X✝ Y✝ X Y : C
c : BinaryCofan X Y
cofans : (X Y : C) → BinaryCofan X Y
colimits : (X Y : C) → IsColimit (cofans X Y)
cones : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → PullbackCone f g
limits : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → IsLimit (cones f g)
h₁ :
  ∀ {X' Y' : C} (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : (cofans X' Y').pt ⟶ c.pt),
    αX ≫ BinaryCofan.inl c = BinaryCofan.inl (cofans X' Y') ≫ f →
      αY ≫ BinaryCofan.inr c = BinaryCofan.inr (cofans X' Y') ≫ f →
        IsPullback (BinaryCofan.inl (cofans X' Y')) αX f (BinaryCofan.inl c) ∧
          IsPullback (BinaryCofan.inr (cofans X' Y')) αY f (BinaryCofan.inr c)
h₂ :
  {Z : C} →
    (f : Z ⟶ c.pt) →
      IsColimit
        (BinaryCofan.mk (PullbackCone.fst (cones f (BinaryCofan.inl c)))
          (PullbackCone.fst (cones f (BinaryCofan.inr c))))
X' Y' : C
c' : BinaryCofan X' Y'
αX : X' ⟶ X
αY : Y' ⟶ Y
f : c'.pt ⟶ c.pt
hX : αX ≫ BinaryCofan.inl c = BinaryCofan.inl c' ≫ f
hY : αY ≫ BinaryCofan.inr c = BinaryCofan.inr c' ≫ f
H₁ : IsPullback (BinaryCofan.inl c') αX f (BinaryCofan.inl c)
H₂ : IsPullback (BinaryCofan.inr c') αY f (BinaryCofan.inr c)
e₁ : X' ≅ (cones f (BinaryCofan.inl c)).pt :=
  IsLimit.conePointUniqueUpToIso (IsPullback.isLimit H₁) (limits f (BinaryCofan.inl c))
e₂ : Y' ≅ (cones f (BinaryCofan.inr c)).pt :=
  IsLimit.conePointUniqueUpToIso (IsPullback.isLimit H₂) (limits f (BinaryCofan.inr c))
he₁ : BinaryCofan.inl c' = e₁.hom ≫ PullbackCone.fst (cones f (BinaryCofan.inl c))
he₂ : BinaryCofan.inr c' = e₂.hom ≫ PullbackCone.fst (cones f (BinaryCofan.inr c))
⊢ IsColimit (BinaryCofan.mk (BinaryCofan.inl c') (BinaryCofan.inr c'))
rw [he₁, he₂]
case mpr.intro.h
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
X✝ Y✝ X Y : C
c : BinaryCofan X Y
cofans : (X Y : C) → BinaryCofan X Y
colimits : (X Y : C) → IsColimit (cofans X Y)
cones : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → PullbackCone f g
limits : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → IsLimit (cones f g)
h₁ :
  ∀ {X' Y' : C} (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : (cofans X' Y').pt ⟶ c.pt),
    αX ≫ BinaryCofan.inl c = BinaryCofan.inl (cofans X' Y') ≫ f →
      αY ≫ BinaryCofan.inr c = BinaryCofan.inr (cofans X' Y') ≫ f →
        IsPullback (BinaryCofan.inl (cofans X' Y')) αX f (BinaryCofan.inl c) ∧
          IsPullback (BinaryCofan.inr (cofans X' Y')) αY f (BinaryCofan.inr c)
h₂ :
  {Z : C} →
    (f : Z ⟶ c.pt) →
      IsColimit
        (BinaryCofan.mk (PullbackCone.fst (cones f (BinaryCofan.inl c)))
          (PullbackCone.fst (cones f (BinaryCofan.inr c))))
X' Y' : C
c' : BinaryCofan X' Y'
αX : X' ⟶ X
αY : Y' ⟶ Y
f : c'.pt ⟶ c.pt
hX : αX ≫ BinaryCofan.inl c = BinaryCofan.inl c' ≫ f
hY : αY ≫ BinaryCofan.inr c = BinaryCofan.inr c' ≫ f
H₁ : IsPullback (BinaryCofan.inl c') αX f (BinaryCofan.inl c)
H₂ : IsPullback (BinaryCofan.inr c') αY f (BinaryCofan.inr c)
e₁ : X' ≅ (cones f (BinaryCofan.inl c)).pt :=
  IsLimit.conePointUniqueUpToIso (IsPullback.isLimit H₁) (limits f (BinaryCofan.inl c))
e₂ : Y' ≅ (cones f (BinaryCofan.inr c)).pt :=
  IsLimit.conePointUniqueUpToIso (IsPullback.isLimit H₂) (limits f (BinaryCofan.inr c))
he₁ : BinaryCofan.inl c' = e₁.hom ≫ PullbackCone.fst (cones f (BinaryCofan.inl c))
he₂ : BinaryCofan.inr c' = e₂.hom ≫ PullbackCone.fst (cones f (BinaryCofan.inr c))
⊢ IsColimit
    (BinaryCofan.mk (e₁.hom ≫ PullbackCone.fst (cones f (BinaryCofan.inl c)))
      ((cones f (BinaryCofan.inr c)).π.1 WalkingCospan.left))
case mpr.intro
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
X✝ Y✝ X Y : C
c : BinaryCofan X Y
cofans : (X Y : C) → BinaryCofan X Y
colimits : (X Y : C) → IsColimit (cofans X Y)
cones : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → PullbackCone f g
limits : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → IsLimit (cones f g)
h₁ :
  ∀ {X' Y' : C} (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : (cofans X' Y').pt ⟶ c.pt),
    αX ≫ BinaryCofan.inl c = BinaryCofan.inl (cofans X' Y') ≫ f →
      αY ≫ BinaryCofan.inr c = BinaryCofan.inr (cofans X' Y') ≫ f →
        IsPullback (BinaryCofan.inl (cofans X' Y')) αX f (BinaryCofan.inl c) ∧
          IsPullback (BinaryCofan.inr (cofans X' Y')) αY f (BinaryCofan.inr c)
h₂ :
  {Z : C} →
    (f : Z ⟶ c.pt) →
      IsColimit
        (BinaryCofan.mk (PullbackCone.fst (cones f (BinaryCofan.inl c)))
          (PullbackCone.fst (cones f (BinaryCofan.inr c))))
X' Y' : C
c' : BinaryCofan X' Y'
αX : X' ⟶ X
αY : Y' ⟶ Y
f : c'.pt ⟶ c.pt
hX : αX ≫ BinaryCofan.inl c = BinaryCofan.inl c' ≫ f
hY : αY ≫ BinaryCofan.inr c = BinaryCofan.inr c' ≫ f
H₁ : IsPullback (BinaryCofan.inl c') αX f (BinaryCofan.inl c)
H₂ : IsPullback (BinaryCofan.inr c') αY f (BinaryCofan.inr c)
e₁ : X' ≅ (cones f (BinaryCofan.inl c)).pt :=
  IsLimit.conePointUniqueUpToIso (IsPullback.isLimit H₁) (limits f (BinaryCofan.inl c))
e₂ : Y' ≅ (cones f (BinaryCofan.inr c)).pt :=
  IsLimit.conePointUniqueUpToIso (IsPullback.isLimit H₂) (limits f (BinaryCofan.inr c))
he₁ : BinaryCofan.inl c' = e₁.hom ≫ PullbackCone.fst (cones f (BinaryCofan.inl c))
he₂ : BinaryCofan.inr c' = e₂.hom ≫ PullbackCone.fst (cones f (BinaryCofan.inr c))
⊢ IsColimit
    (BinaryCofan.mk (e₁.hom ≫ PullbackCone.fst (cones f (BinaryCofan.inl c)))
      (e₂.hom ≫ PullbackCone.fst (cones f (BinaryCofan.inr c))))
apply BinaryCofan.isColimitCompRightIso (BinaryCofan.mk _ _)
case mpr.intro.h.h
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
X✝ Y✝ X Y : C
c : BinaryCofan X Y
cofans : (X Y : C) → BinaryCofan X Y
colimits : (X Y : C) → IsColimit (cofans X Y)
cones : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → PullbackCone f g
limits : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → IsLimit (cones f g)
h₁ :
  ∀ {X' Y' : C} (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : (cofans X' Y').pt ⟶ c.pt),
    αX ≫ BinaryCofan.inl c = BinaryCofan.inl (cofans X' Y') ≫ f →
      αY ≫ BinaryCofan.inr c = BinaryCofan.inr (cofans X' Y') ≫ f →
        IsPullback (BinaryCofan.inl (cofans X' Y')) αX f (BinaryCofan.inl c) ∧
          IsPullback (BinaryCofan.inr (cofans X' Y')) αY f (BinaryCofan.inr c)
h₂ :
  {Z : C} →
    (f : Z ⟶ c.pt) →
      IsColimit
        (BinaryCofan.mk (PullbackCone.fst (cones f (BinaryCofan.inl c)))
          (PullbackCone.fst (cones f (BinaryCofan.inr c))))
X' Y' : C
c' : BinaryCofan X' Y'
αX : X' ⟶ X
αY : Y' ⟶ Y
f : c'.pt ⟶ c.pt
hX : αX ≫ BinaryCofan.inl c = BinaryCofan.inl c' ≫ f
hY : αY ≫ BinaryCofan.inr c = BinaryCofan.inr c' ≫ f
H₁ : IsPullback (BinaryCofan.inl c') αX f (BinaryCofan.inl c)
H₂ : IsPullback (BinaryCofan.inr c') αY f (BinaryCofan.inr c)
e₁ : X' ≅ (cones f (BinaryCofan.inl c)).pt :=
  IsLimit.conePointUniqueUpToIso (IsPullback.isLimit H₁) (limits f (BinaryCofan.inl c))
e₂ : Y' ≅ (cones f (BinaryCofan.inr c)).pt :=
  IsLimit.conePointUniqueUpToIso (IsPullback.isLimit H₂) (limits f (BinaryCofan.inr c))
he₁ : BinaryCofan.inl c' = e₁.hom ≫ PullbackCone.fst (cones f (BinaryCofan.inl c))
he₂ : BinaryCofan.inr c' = e₂.hom ≫ PullbackCone.fst (cones f (BinaryCofan.inr c))
⊢ IsColimit
    (BinaryCofan.mk ((cones f (BinaryCofan.inl c)).π.1 WalkingCospan.left)
      ((cones f (BinaryCofan.inr c)).π.1 WalkingCospan.left))
case mpr.intro.h
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
X✝ Y✝ X Y : C
c : BinaryCofan X Y
cofans : (X Y : C) → BinaryCofan X Y
colimits : (X Y : C) → IsColimit (cofans X Y)
cones : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → PullbackCone f g
limits : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → IsLimit (cones f g)
h₁ :
  ∀ {X' Y' : C} (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : (cofans X' Y').pt ⟶ c.pt),
    αX ≫ BinaryCofan.inl c = BinaryCofan.inl (cofans X' Y') ≫ f →
      αY ≫ BinaryCofan.inr c = BinaryCofan.inr (cofans X' Y') ≫ f →
        IsPullback (BinaryCofan.inl (cofans X' Y')) αX f (BinaryCofan.inl c) ∧
          IsPullback (BinaryCofan.inr (cofans X' Y')) αY f (BinaryCofan.inr c)
h₂ :
  {Z : C} →
    (f : Z ⟶ c.pt) →
      IsColimit
        (BinaryCofan.mk (PullbackCone.fst (cones f (BinaryCofan.inl c)))
          (PullbackCone.fst (cones f (BinaryCofan.inr c))))
X' Y' : C
c' : BinaryCofan X' Y'
αX : X' ⟶ X
αY : Y' ⟶ Y
f : c'.pt ⟶ c.pt
hX : αX ≫ BinaryCofan.inl c = BinaryCofan.inl c' ≫ f
hY : αY ≫ BinaryCofan.inr c = BinaryCofan.inr c' ≫ f
H₁ : IsPullback (BinaryCofan.inl c') αX f (BinaryCofan.inl c)
H₂ : IsPullback (BinaryCofan.inr c') αY f (BinaryCofan.inr c)
e₁ : X' ≅ (cones f (BinaryCofan.inl c)).pt :=
  IsLimit.conePointUniqueUpToIso (IsPullback.isLimit H₁) (limits f (BinaryCofan.inl c))
e₂ : Y' ≅ (cones f (BinaryCofan.inr c)).pt :=
  IsLimit.conePointUniqueUpToIso (IsPullback.isLimit H₂) (limits f (BinaryCofan.inr c))
he₁ : BinaryCofan.inl c' = e₁.hom ≫ PullbackCone.fst (cones f (BinaryCofan.inl c))
he₂ : BinaryCofan.inr c' = e₂.hom ≫ PullbackCone.fst (cones f (BinaryCofan.inr c))
⊢ IsColimit
    (BinaryCofan.mk (e₁.hom ≫ PullbackCone.fst (cones f (BinaryCofan.inl c)))
      ((cones f (BinaryCofan.inr c)).π.1 WalkingCospan.left))
apply BinaryCofan.isColimitCompLeftIso (BinaryCofan.mk _ _)
no goals
case mpr.intro.h.h
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
X✝ Y✝ X Y : C
c : BinaryCofan X Y
cofans : (X Y : C) → BinaryCofan X Y
colimits : (X Y : C) → IsColimit (cofans X Y)
cones : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → PullbackCone f g
limits : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → IsLimit (cones f g)
h₁ :
  ∀ {X' Y' : C} (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : (cofans X' Y').pt ⟶ c.pt),
    αX ≫ BinaryCofan.inl c = BinaryCofan.inl (cofans X' Y') ≫ f →
      αY ≫ BinaryCofan.inr c = BinaryCofan.inr (cofans X' Y') ≫ f →
        IsPullback (BinaryCofan.inl (cofans X' Y')) αX f (BinaryCofan.inl c) ∧
          IsPullback (BinaryCofan.inr (cofans X' Y')) αY f (BinaryCofan.inr c)
h₂ :
  {Z : C} →
    (f : Z ⟶ c.pt) →
      IsColimit
        (BinaryCofan.mk (PullbackCone.fst (cones f (BinaryCofan.inl c)))
          (PullbackCone.fst (cones f (BinaryCofan.inr c))))
X' Y' : C
c' : BinaryCofan X' Y'
αX : X' ⟶ X
αY : Y' ⟶ Y
f : c'.pt ⟶ c.pt
hX : αX ≫ BinaryCofan.inl c = BinaryCofan.inl c' ≫ f
hY : αY ≫ BinaryCofan.inr c = BinaryCofan.inr c' ≫ f
H₁ : IsPullback (BinaryCofan.inl c') αX f (BinaryCofan.inl c)
H₂ : IsPullback (BinaryCofan.inr c') αY f (BinaryCofan.inr c)
e₁ : X' ≅ (cones f (BinaryCofan.inl c)).pt :=
  IsLimit.conePointUniqueUpToIso (IsPullback.isLimit H₁) (limits f (BinaryCofan.inl c))
e₂ : Y' ≅ (cones f (BinaryCofan.inr c)).pt :=
  IsLimit.conePointUniqueUpToIso (IsPullback.isLimit H₂) (limits f (BinaryCofan.inr c))
he₁ : BinaryCofan.inl c' = e₁.hom ≫ PullbackCone.fst (cones f (BinaryCofan.inl c))
he₂ : BinaryCofan.inr c' = e₂.hom ≫ PullbackCone.fst (cones f (BinaryCofan.inr c))
⊢ IsColimit
    (BinaryCofan.mk ((cones f (BinaryCofan.inl c)).π.1 WalkingCospan.left)
      ((cones f (BinaryCofan.inr c)).π.1 WalkingCospan.left))
exact h₂ f
no goals
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
X✝ Y✝ X Y : C
c : BinaryCofan X Y
cofans : (X Y : C) → BinaryCofan X Y
colimits : (X Y : C) → IsColimit (cofans X Y)
cones : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → PullbackCone f g
limits : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → IsLimit (cones f g)
h₁ :
  ∀ {X' Y' : C} (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : (cofans X' Y').pt ⟶ c.pt),
    αX ≫ BinaryCofan.inl c = BinaryCofan.inl (cofans X' Y') ≫ f →
      αY ≫ BinaryCofan.inr c = BinaryCofan.inr (cofans X' Y') ≫ f →
        IsPullback (BinaryCofan.inl (cofans X' Y')) αX f (BinaryCofan.inl c) ∧
          IsPullback (BinaryCofan.inr (cofans X' Y')) αY f (BinaryCofan.inr c)
h₂ :
  {Z : C} →
    (f : Z ⟶ c.pt) →
      IsColimit
        (BinaryCofan.mk (PullbackCone.fst (cones f (BinaryCofan.inl c)))
          (PullbackCone.fst (cones f (BinaryCofan.inr c))))
X' Y' : C
c' : BinaryCofan X' Y'
αX : X' ⟶ X
αY : Y' ⟶ Y
f : c'.pt ⟶ c.pt
hX : αX ≫ BinaryCofan.inl c = BinaryCofan.inl c' ≫ f
hY : αY ≫ BinaryCofan.inr c = BinaryCofan.inr c' ≫ f
H₁ : IsPullback (BinaryCofan.inl c') αX f (BinaryCofan.inl c)
H₂ : IsPullback (BinaryCofan.inr c') αY f (BinaryCofan.inr c)
e₁ : X' ≅ (cones f (BinaryCofan.inl c)).pt :=
  IsLimit.conePointUniqueUpToIso (IsPullback.isLimit H₁) (limits f (BinaryCofan.inl c))
e₂ : Y' ≅ (cones f (BinaryCofan.inr c)).pt :=
  IsLimit.conePointUniqueUpToIso (IsPullback.isLimit H₂) (limits f (BinaryCofan.inr c))
⊢ BinaryCofan.inl c' = e₁.hom ≫ PullbackCone.fst (cones f (BinaryCofan.inl c))
simp
no goals
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
X✝ Y✝ X Y : C
c : BinaryCofan X Y
cofans : (X Y : C) → BinaryCofan X Y
colimits : (X Y : C) → IsColimit (cofans X Y)
cones : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → PullbackCone f g
limits : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → IsLimit (cones f g)
h₁ :
  ∀ {X' Y' : C} (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : (cofans X' Y').pt ⟶ c.pt),
    αX ≫ BinaryCofan.inl c = BinaryCofan.inl (cofans X' Y') ≫ f →
      αY ≫ BinaryCofan.inr c = BinaryCofan.inr (cofans X' Y') ≫ f →
        IsPullback (BinaryCofan.inl (cofans X' Y')) αX f (BinaryCofan.inl c) ∧
          IsPullback (BinaryCofan.inr (cofans X' Y')) αY f (BinaryCofan.inr c)
h₂ :
  {Z : C} →
    (f : Z ⟶ c.pt) →
      IsColimit
        (BinaryCofan.mk (PullbackCone.fst (cones f (BinaryCofan.inl c)))
          (PullbackCone.fst (cones f (BinaryCofan.inr c))))
X' Y' : C
c' : BinaryCofan X' Y'
αX : X' ⟶ X
αY : Y' ⟶ Y
f : c'.pt ⟶ c.pt
hX : αX ≫ BinaryCofan.inl c = BinaryCofan.inl c' ≫ f
hY : αY ≫ BinaryCofan.inr c = BinaryCofan.inr c' ≫ f
H₁ : IsPullback (BinaryCofan.inl c') αX f (BinaryCofan.inl c)
H₂ : IsPullback (BinaryCofan.inr c') αY f (BinaryCofan.inr c)
e₁ : X' ≅ (cones f (BinaryCofan.inl c)).pt :=
  IsLimit.conePointUniqueUpToIso (IsPullback.isLimit H₁) (limits f (BinaryCofan.inl c))
e₂ : Y' ≅ (cones f (BinaryCofan.inr c)).pt :=
  IsLimit.conePointUniqueUpToIso (IsPullback.isLimit H₂) (limits f (BinaryCofan.inr c))
he₁ : BinaryCofan.inl c' = e₁.hom ≫ PullbackCone.fst (cones f (BinaryCofan.inl c))
⊢ BinaryCofan.inr c' = e₂.hom ≫ PullbackCone.fst (cones f (BinaryCofan.inr c))
simp