J : Type v'
inst✝² : Category J
C : Type u
inst✝¹ : Category C
inst✝ : HasStrictInitialObjects C
X : C
h : IsInitial X
F' : Discrete PEmpty ⥤ C
c' : Cocone F'
α : F' ⟶ Functor.empty C
f : c'.pt ⟶ (asEmptyCocone X).pt
hf : α ≫ (asEmptyCocone X).ι = c'.ι ≫ (Functor.const (Discrete PEmpty)).map f
hα : NatTrans.Equifibered α
⊢ Nonempty (IsColimit c') ↔ ∀ (j : Discrete PEmpty), IsPullback (c'.ι.app j) (α.app j) f ((asEmptyCocone X).ι.app j)
J : Type v'
inst✝² : Category J
C : Type u
inst✝¹ : Category C
inst✝ : HasStrictInitialObjects C
X : C
h : IsInitial X
⊢ IsVanKampenColimit (asEmptyCocone X)
intro F' c' α f hf hα
J : Type v'
inst✝² : Category J
C : Type u
inst✝¹ : Category C
inst✝ : HasStrictInitialObjects C
X : C
h : IsInitial X
F' : Discrete PEmpty ⥤ C
c' : Cocone F'
α : F' ⟶ Functor.empty C
f : c'.pt ⟶ (asEmptyCocone X).pt
hf : α ≫ (asEmptyCocone X).ι = c'.ι ≫ (Functor.const (Discrete PEmpty)).map f
hα : NatTrans.Equifibered α
this : F' = Functor.empty C
⊢ Nonempty (IsColimit c') ↔ ∀ (j : Discrete PEmpty), IsPullback (c'.ι.app j) (α.app j) f ((asEmptyCocone X).ι.app j)
J : Type v'
inst✝² : Category J
C : Type u
inst✝¹ : Category C
inst✝ : HasStrictInitialObjects C
X : C
h : IsInitial X
F' : Discrete PEmpty ⥤ C
c' : Cocone F'
α : F' ⟶ Functor.empty C
f : c'.pt ⟶ (asEmptyCocone X).pt
hf : α ≫ (asEmptyCocone X).ι = c'.ι ≫ (Functor.const (Discrete PEmpty)).map f
hα : NatTrans.Equifibered α
⊢ Nonempty (IsColimit c') ↔ ∀ (j : Discrete PEmpty), IsPullback (c'.ι.app j) (α.app j) f ((asEmptyCocone X).ι.app j)
have : F' = Functor.empty C := by apply Functor.hext <;> rintro ⟨⟨⟩⟩
J : Type v'
inst✝² : Category J
C : Type u
inst✝¹ : Category C
inst✝ : HasStrictInitialObjects C
X : C
h : IsInitial X
c' : Cocone (Functor.empty C)
α : Functor.empty C ⟶ Functor.empty C
f : c'.pt ⟶ (asEmptyCocone X).pt
hf : α ≫ (asEmptyCocone X).ι = c'.ι ≫ (Functor.const (Discrete PEmpty)).map f
hα : NatTrans.Equifibered α
⊢ Nonempty (IsColimit c') ↔ ∀ (j : Discrete PEmpty), IsPullback (c'.ι.app j) (α.app j) f ((asEmptyCocone X).ι.app j)
J : Type v'
inst✝² : Category J
C : Type u
inst✝¹ : Category C
inst✝ : HasStrictInitialObjects C
X : C
h : IsInitial X
F' : Discrete PEmpty ⥤ C
c' : Cocone F'
α : F' ⟶ Functor.empty C
f : c'.pt ⟶ (asEmptyCocone X).pt
hf : α ≫ (asEmptyCocone X).ι = c'.ι ≫ (Functor.const (Discrete PEmpty)).map f
hα : NatTrans.Equifibered α
this : F' = Functor.empty C
⊢ Nonempty (IsColimit c') ↔ ∀ (j : Discrete PEmpty), IsPullback (c'.ι.app j) (α.app j) f ((asEmptyCocone X).ι.app j)
subst this
J : Type v'
inst✝² : Category J
C : Type u
inst✝¹ : Category C
inst✝ : HasStrictInitialObjects C
X : C
h : IsInitial X
c' : Cocone (Functor.empty C)
α : Functor.empty C ⟶ Functor.empty C
f : c'.pt ⟶ (asEmptyCocone X).pt
hf : α ≫ (asEmptyCocone X).ι = c'.ι ≫ (Functor.const (Discrete PEmpty)).map f
hα : NatTrans.Equifibered α
this : IsIso f
⊢ Nonempty (IsColimit c') ↔ ∀ (j : Discrete PEmpty), IsPullback (c'.ι.app j) (α.app j) f ((asEmptyCocone X).ι.app j)
J : Type v'
inst✝² : Category J
C : Type u
inst✝¹ : Category C
inst✝ : HasStrictInitialObjects C
X : C
h : IsInitial X
c' : Cocone (Functor.empty C)
α : Functor.empty C ⟶ Functor.empty C
f : c'.pt ⟶ (asEmptyCocone X).pt
hf : α ≫ (asEmptyCocone X).ι = c'.ι ≫ (Functor.const (Discrete PEmpty)).map f
hα : NatTrans.Equifibered α
⊢ Nonempty (IsColimit c') ↔ ∀ (j : Discrete PEmpty), IsPullback (c'.ι.app j) (α.app j) f ((asEmptyCocone X).ι.app j)
haveI := h.isIso_to f
no goals
J : Type v'
inst✝² : Category J
C : Type u
inst✝¹ : Category C
inst✝ : HasStrictInitialObjects C
X : C
h : IsInitial X
c' : Cocone (Functor.empty C)
α : Functor.empty C ⟶ Functor.empty C
f : c'.pt ⟶ (asEmptyCocone X).pt
hf : α ≫ (asEmptyCocone X).ι = c'.ι ≫ (Functor.const (Discrete PEmpty)).map f
hα : NatTrans.Equifibered α
this : IsIso f
⊢ Nonempty (IsColimit c') ↔ ∀ (j : Discrete PEmpty), IsPullback (c'.ι.app j) (α.app j) f ((asEmptyCocone X).ι.app j)
refine' ⟨by rintro _ ⟨⟨⟩⟩,
  fun _ => ⟨IsColimit.ofIsoColimit h (Cocones.ext (asIso f).symm <| by rintro ⟨⟨⟩⟩)⟩⟩
no goals
J : Type v'
inst✝² : Category J
C : Type u
inst✝¹ : Category C
inst✝ : HasStrictInitialObjects C
X : C
h : IsInitial X
F' : Discrete PEmpty ⥤ C
c' : Cocone F'
α : F' ⟶ Functor.empty C
f : c'.pt ⟶ (asEmptyCocone X).pt
hf : α ≫ (asEmptyCocone X).ι = c'.ι ≫ (Functor.const (Discrete PEmpty)).map f
hα : NatTrans.Equifibered α
⊢ F' = Functor.empty C
apply Functor.hext <;> rintro ⟨⟨⟩⟩
no goals
J : Type v'
inst✝² : Category J
C : Type u
inst✝¹ : Category C
inst✝ : HasStrictInitialObjects C
X : C
h : IsInitial X
c' : Cocone (Functor.empty C)
α : Functor.empty C ⟶ Functor.empty C
f : c'.pt ⟶ (asEmptyCocone X).pt
hf : α ≫ (asEmptyCocone X).ι = c'.ι ≫ (Functor.const (Discrete PEmpty)).map f
hα : NatTrans.Equifibered α
this : IsIso f
⊢ Nonempty (IsColimit c') → ∀ (j : Discrete PEmpty), IsPullback (c'.ι.app j) (α.app j) f ((asEmptyCocone X).ι.app j)
rintro _ ⟨⟨⟩⟩
no goals
J : Type v'
inst✝² : Category J
C : Type u
inst✝¹ : Category C
inst✝ : HasStrictInitialObjects C
X : C
h : IsInitial X
c' : Cocone (Functor.empty C)
α : Functor.empty C ⟶ Functor.empty C
f : c'.pt ⟶ (asEmptyCocone X).pt
hf : α ≫ (asEmptyCocone X).ι = c'.ι ≫ (Functor.const (Discrete PEmpty)).map f
hα : NatTrans.Equifibered α
this : IsIso f
x✝ : ∀ (j : Discrete PEmpty), IsPullback (c'.ι.app j) (α.app j) f ((asEmptyCocone X).ι.app j)
⊢ ∀ (j : Discrete PEmpty), (asEmptyCocone X).ι.app j ≫ (asIso f).symm.hom = c'.ι.app j
rintro ⟨⟨⟩⟩