J : Type v'
inst✝⁴ : Category J
C : Type u
inst✝³ : Category C
X Y : C
D : Type u''
inst✝² : Category D
inst✝¹ : HasPullbacks D
inst✝ : HasColimitsOfShape J D
F : J ⥤ C ⥤ D
c : Cocone F
hc : ∀ (x : C), IsVanKampenColimit (((evaluation C D).obj x).mapCocone c)
F' : J ⥤ C ⥤ D
c' : Cocone F'
α : F' ⟶ F
f : c'.pt ⟶ c.pt
e : α ≫ c.ι = c'.ι ≫ (Functor.const J).map f
hα : NatTrans.Equifibered α
⊢ Nonempty (IsColimit c') ↔ ∀ (j : J), IsPullback (c'.ι.app j) (α.app j) f (c.ι.app j)
J : Type v'
inst✝⁴ : Category J
C : Type u
inst✝³ : Category C
X Y : C
D : Type u''
inst✝² : Category D
inst✝¹ : HasPullbacks D
inst✝ : HasColimitsOfShape J D
F : J ⥤ C ⥤ D
c : Cocone F
hc : ∀ (x : C), IsVanKampenColimit (((evaluation C D).obj x).mapCocone c)
⊢ IsVanKampenColimit c
intro F' c' α f e hα
J : Type v'
inst✝⁴ : Category J
C : Type u
inst✝³ : Category C
X Y : C
D : Type u''
inst✝² : Category D
inst✝¹ : HasPullbacks D
inst✝ : HasColimitsOfShape J D
F : J ⥤ C ⥤ D
c : Cocone F
hc : ∀ (x : C), IsVanKampenColimit (((evaluation C D).obj x).mapCocone c)
F' : J ⥤ C ⥤ D
c' : Cocone F'
α : F' ⟶ F
f : c'.pt ⟶ c.pt
e : α ≫ c.ι = c'.ι ≫ (Functor.const J).map f
hα : NatTrans.Equifibered α
this :
  ∀ (x : C),
    Nonempty (IsColimit (((evaluation C D).obj x).mapCocone c')) ↔
      ∀ (j : J),
        IsPullback ((((evaluation C D).obj x).mapCocone c').ι.app j) ((whiskerRight α ((evaluation C D).obj x)).app j)
          (((evaluation C D).obj x).map f) ((((evaluation C D).obj x).mapCocone c).ι.app j)
⊢ Nonempty (IsColimit c') ↔ ∀ (j : J), IsPullback (c'.ι.app j) (α.app j) f (c.ι.app j)
J : Type v'
inst✝⁴ : Category J
C : Type u
inst✝³ : Category C
X Y : C
D : Type u''
inst✝² : Category D
inst✝¹ : HasPullbacks D
inst✝ : HasColimitsOfShape J D
F : J ⥤ C ⥤ D
c : Cocone F
hc : ∀ (x : C), IsVanKampenColimit (((evaluation C D).obj x).mapCocone c)
F' : J ⥤ C ⥤ D
c' : Cocone F'
α : F' ⟶ F
f : c'.pt ⟶ c.pt
e : α ≫ c.ι = c'.ι ≫ (Functor.const J).map f
hα : NatTrans.Equifibered α
⊢ Nonempty (IsColimit c') ↔ ∀ (j : J), IsPullback (c'.ι.app j) (α.app j) f (c.ι.app j)
have := fun x => hc x (((evaluation C D).obj x).mapCocone c') (whiskerRight α _)
    (((evaluation C D).obj x).map f)
    (by
      ext y
      dsimp
      exact NatTrans.congr_app (NatTrans.congr_app e y) x)
    (hα.whiskerRight _)
case mp
J : Type v'
inst✝⁴ : Category J
C : Type u
inst✝³ : Category C
X Y : C
D : Type u''
inst✝² : Category D
inst✝¹ : HasPullbacks D
inst✝ : HasColimitsOfShape J D
F : J ⥤ C ⥤ D
c : Cocone F
hc : ∀ (x : C), IsVanKampenColimit (((evaluation C D).obj x).mapCocone c)
F' : J ⥤ C ⥤ D
c' : Cocone F'
α : F' ⟶ F
f : c'.pt ⟶ c.pt
e : α ≫ c.ι = c'.ι ≫ (Functor.const J).map f
hα : NatTrans.Equifibered α
this :
  ∀ (x : C),
    Nonempty (IsColimit (((evaluation C D).obj x).mapCocone c')) ↔
      ∀ (j : J),
        IsPullback ((((evaluation C D).obj x).mapCocone c').ι.app j) ((whiskerRight α ((evaluation C D).obj x)).app j)
          (((evaluation C D).obj x).map f) ((((evaluation C D).obj x).mapCocone c).ι.app j)
⊢ Nonempty (IsColimit c') → ∀ (j : J), IsPullback (c'.ι.app j) (α.app j) f (c.ι.app j)

case mpr
J : Type v'
inst✝⁴ : Category J
C : Type u
inst✝³ : Category C
X Y : C
D : Type u''
inst✝² : Category D
inst✝¹ : HasPullbacks D
inst✝ : HasColimitsOfShape J D
F : J ⥤ C ⥤ D
c : Cocone F
hc : ∀ (x : C), IsVanKampenColimit (((evaluation C D).obj x).mapCocone c)
F' : J ⥤ C ⥤ D
c' : Cocone F'
α : F' ⟶ F
f : c'.pt ⟶ c.pt
e : α ≫ c.ι = c'.ι ≫ (Functor.const J).map f
hα : NatTrans.Equifibered α
this :
  ∀ (x : C),
    Nonempty (IsColimit (((evaluation C D).obj x).mapCocone c')) ↔
      ∀ (j : J),
        IsPullback ((((evaluation C D).obj x).mapCocone c').ι.app j) ((whiskerRight α ((evaluation C D).obj x)).app j)
          (((evaluation C D).obj x).map f) ((((evaluation C D).obj x).mapCocone c).ι.app j)
⊢ (∀ (j : J), IsPullback (c'.ι.app j) (α.app j) f (c.ι.app j)) → Nonempty (IsColimit c')
J : Type v'
inst✝⁴ : Category J
C : Type u
inst✝³ : Category C
X Y : C
D : Type u''
inst✝² : Category D
inst✝¹ : HasPullbacks D
inst✝ : HasColimitsOfShape J D
F : J ⥤ C ⥤ D
c : Cocone F
hc : ∀ (x : C), IsVanKampenColimit (((evaluation C D).obj x).mapCocone c)
F' : J ⥤ C ⥤ D
c' : Cocone F'
α : F' ⟶ F
f : c'.pt ⟶ c.pt
e : α ≫ c.ι = c'.ι ≫ (Functor.const J).map f
hα : NatTrans.Equifibered α
this :
  ∀ (x : C),
    Nonempty (IsColimit (((evaluation C D).obj x).mapCocone c')) ↔
      ∀ (j : J),
        IsPullback ((((evaluation C D).obj x).mapCocone c').ι.app j) ((whiskerRight α ((evaluation C D).obj x)).app j)
          (((evaluation C D).obj x).map f) ((((evaluation C D).obj x).mapCocone c).ι.app j)
⊢ Nonempty (IsColimit c') ↔ ∀ (j : J), IsPullback (c'.ι.app j) (α.app j) f (c.ι.app j)
constructor
case w.h
J : Type v'
inst✝⁴ : Category J
C : Type u
inst✝³ : Category C
X Y : C
D : Type u''
inst✝² : Category D
inst✝¹ : HasPullbacks D
inst✝ : HasColimitsOfShape J D
F : J ⥤ C ⥤ D
c : Cocone F
hc : ∀ (x : C), IsVanKampenColimit (((evaluation C D).obj x).mapCocone c)
F' : J ⥤ C ⥤ D
c' : Cocone F'
α : F' ⟶ F
f : c'.pt ⟶ c.pt
e : α ≫ c.ι = c'.ι ≫ (Functor.const J).map f
hα : NatTrans.Equifibered α
x : C
y : J
⊢ (whiskerRight α ((evaluation C D).obj x) ≫ (((evaluation C D).obj x).mapCocone c).ι).app y =
    ((((evaluation C D).obj x).mapCocone c').ι ≫ (Functor.const J).map (((evaluation C D).obj x).map f)).app y
J : Type v'
inst✝⁴ : Category J
C : Type u
inst✝³ : Category C
X Y : C
D : Type u''
inst✝² : Category D
inst✝¹ : HasPullbacks D
inst✝ : HasColimitsOfShape J D
F : J ⥤ C ⥤ D
c : Cocone F
hc : ∀ (x : C), IsVanKampenColimit (((evaluation C D).obj x).mapCocone c)
F' : J ⥤ C ⥤ D
c' : Cocone F'
α : F' ⟶ F
f : c'.pt ⟶ c.pt
e : α ≫ c.ι = c'.ι ≫ (Functor.const J).map f
hα : NatTrans.Equifibered α
x : C
⊢ whiskerRight α ((evaluation C D).obj x) ≫ (((evaluation C D).obj x).mapCocone c).ι =
    (((evaluation C D).obj x).mapCocone c').ι ≫ (Functor.const J).map (((evaluation C D).obj x).map f)
ext y
case w.h
J : Type v'
inst✝⁴ : Category J
C : Type u
inst✝³ : Category C
X Y : C
D : Type u''
inst✝² : Category D
inst✝¹ : HasPullbacks D
inst✝ : HasColimitsOfShape J D
F : J ⥤ C ⥤ D
c : Cocone F
hc : ∀ (x : C), IsVanKampenColimit (((evaluation C D).obj x).mapCocone c)
F' : J ⥤ C ⥤ D
c' : Cocone F'
α : F' ⟶ F
f : c'.pt ⟶ c.pt
e : α ≫ c.ι = c'.ι ≫ (Functor.const J).map f
hα : NatTrans.Equifibered α
x : C
y : J
⊢ (α.app y).app x ≫ (c.ι.app y).app x = (c'.ι.app y).app x ≫ f.app x
case w.h
J : Type v'
inst✝⁴ : Category J
C : Type u
inst✝³ : Category C
X Y : C
D : Type u''
inst✝² : Category D
inst✝¹ : HasPullbacks D
inst✝ : HasColimitsOfShape J D
F : J ⥤ C ⥤ D
c : Cocone F
hc : ∀ (x : C), IsVanKampenColimit (((evaluation C D).obj x).mapCocone c)
F' : J ⥤ C ⥤ D
c' : Cocone F'
α : F' ⟶ F
f : c'.pt ⟶ c.pt
e : α ≫ c.ι = c'.ι ≫ (Functor.const J).map f
hα : NatTrans.Equifibered α
x : C
y : J
⊢ (whiskerRight α ((evaluation C D).obj x) ≫ (((evaluation C D).obj x).mapCocone c).ι).app y =
    ((((evaluation C D).obj x).mapCocone c').ι ≫ (Functor.const J).map (((evaluation C D).obj x).map f)).app y
dsimp
no goals
case w.h
J : Type v'
inst✝⁴ : Category J
C : Type u
inst✝³ : Category C
X Y : C
D : Type u''
inst✝² : Category D
inst✝¹ : HasPullbacks D
inst✝ : HasColimitsOfShape J D
F : J ⥤ C ⥤ D
c : Cocone F
hc : ∀ (x : C), IsVanKampenColimit (((evaluation C D).obj x).mapCocone c)
F' : J ⥤ C ⥤ D
c' : Cocone F'
α : F' ⟶ F
f : c'.pt ⟶ c.pt
e : α ≫ c.ι = c'.ι ≫ (Functor.const J).map f
hα : NatTrans.Equifibered α
x : C
y : J
⊢ (α.app y).app x ≫ (c.ι.app y).app x = (c'.ι.app y).app x ≫ f.app x
exact NatTrans.congr_app (NatTrans.congr_app e y) x
case mp.intro
J : Type v'
inst✝⁴ : Category J
C : Type u
inst✝³ : Category C
X Y : C
D : Type u''
inst✝² : Category D
inst✝¹ : HasPullbacks D
inst✝ : HasColimitsOfShape J D
F : J ⥤ C ⥤ D
c : Cocone F
hc : ∀ (x : C), IsVanKampenColimit (((evaluation C D).obj x).mapCocone c)
F' : J ⥤ C ⥤ D
c' : Cocone F'
α : F' ⟶ F
f : c'.pt ⟶ c.pt
e : α ≫ c.ι = c'.ι ≫ (Functor.const J).map f
hα : NatTrans.Equifibered α
this :
  ∀ (x : C),
    Nonempty (IsColimit (((evaluation C D).obj x).mapCocone c')) ↔
      ∀ (j : J),
        IsPullback ((((evaluation C D).obj x).mapCocone c').ι.app j) ((whiskerRight α ((evaluation C D).obj x)).app j)
          (((evaluation C D).obj x).map f) ((((evaluation C D).obj x).mapCocone c).ι.app j)
hc' : IsColimit c'
j : J
⊢ IsPullback (c'.ι.app j) (α.app j) f (c.ι.app j)
case mp
J : Type v'
inst✝⁴ : Category J
C : Type u
inst✝³ : Category C
X Y : C
D : Type u''
inst✝² : Category D
inst✝¹ : HasPullbacks D
inst✝ : HasColimitsOfShape J D
F : J ⥤ C ⥤ D
c : Cocone F
hc : ∀ (x : C), IsVanKampenColimit (((evaluation C D).obj x).mapCocone c)
F' : J ⥤ C ⥤ D
c' : Cocone F'
α : F' ⟶ F
f : c'.pt ⟶ c.pt
e : α ≫ c.ι = c'.ι ≫ (Functor.const J).map f
hα : NatTrans.Equifibered α
this :
  ∀ (x : C),
    Nonempty (IsColimit (((evaluation C D).obj x).mapCocone c')) ↔
      ∀ (j : J),
        IsPullback ((((evaluation C D).obj x).mapCocone c').ι.app j) ((whiskerRight α ((evaluation C D).obj x)).app j)
          (((evaluation C D).obj x).map f) ((((evaluation C D).obj x).mapCocone c).ι.app j)
⊢ Nonempty (IsColimit c') → ∀ (j : J), IsPullback (c'.ι.app j) (α.app j) f (c.ι.app j)
rintro ⟨hc'⟩ j
case mp.intro
J : Type v'
inst✝⁴ : Category J
C : Type u
inst✝³ : Category C
X Y : C
D : Type u''
inst✝² : Category D
inst✝¹ : HasPullbacks D
inst✝ : HasColimitsOfShape J D
F : J ⥤ C ⥤ D
c : Cocone F
hc : ∀ (x : C), IsVanKampenColimit (((evaluation C D).obj x).mapCocone c)
F' : J ⥤ C ⥤ D
c' : Cocone F'
α : F' ⟶ F
f : c'.pt ⟶ c.pt
e : α ≫ c.ι = c'.ι ≫ (Functor.const J).map f
hα : NatTrans.Equifibered α
this :
  ∀ (x : C),
    Nonempty (IsColimit (((evaluation C D).obj x).mapCocone c')) ↔
      ∀ (j : J),
        IsPullback ((((evaluation C D).obj x).mapCocone c').ι.app j) ((whiskerRight α ((evaluation C D).obj x)).app j)
          (((evaluation C D).obj x).map f) ((((evaluation C D).obj x).mapCocone c).ι.app j)
hc' : IsColimit c'
j : J
⊢ (k : C) →
    IsLimit
      (((evaluation C D).obj k).mapCone
        (PullbackCone.mk (c'.ι.app j) (α.app j) (_ : c'.ι.app j ≫ f = α.app j ≫ c.ι.app j)))
case mp.intro
J : Type v'
inst✝⁴ : Category J
C : Type u
inst✝³ : Category C
X Y : C
D : Type u''
inst✝² : Category D
inst✝¹ : HasPullbacks D
inst✝ : HasColimitsOfShape J D
F : J ⥤ C ⥤ D
c : Cocone F
hc : ∀ (x : C), IsVanKampenColimit (((evaluation C D).obj x).mapCocone c)
F' : J ⥤ C ⥤ D
c' : Cocone F'
α : F' ⟶ F
f : c'.pt ⟶ c.pt
e : α ≫ c.ι = c'.ι ≫ (Functor.const J).map f
hα : NatTrans.Equifibered α
this :
  ∀ (x : C),
    Nonempty (IsColimit (((evaluation C D).obj x).mapCocone c')) ↔
      ∀ (j : J),
        IsPullback ((((evaluation C D).obj x).mapCocone c').ι.app j) ((whiskerRight α ((evaluation C D).obj x)).app j)
          (((evaluation C D).obj x).map f) ((((evaluation C D).obj x).mapCocone c).ι.app j)
hc' : IsColimit c'
j : J
⊢ IsPullback (c'.ι.app j) (α.app j) f (c.ι.app j)
refine' ⟨⟨(NatTrans.congr_app e j).symm⟩, ⟨evaluationJointlyReflectsLimits _ _⟩⟩
case mp.intro
J : Type v'
inst✝⁴ : Category J
C : Type u
inst✝³ : Category C
X Y : C
D : Type u''
inst✝² : Category D
inst✝¹ : HasPullbacks D
inst✝ : HasColimitsOfShape J D
F : J ⥤ C ⥤ D
c : Cocone F
hc : ∀ (x : C), IsVanKampenColimit (((evaluation C D).obj x).mapCocone c)
F' : J ⥤ C ⥤ D
c' : Cocone F'
α : F' ⟶ F
f : c'.pt ⟶ c.pt
e : α ≫ c.ι = c'.ι ≫ (Functor.const J).map f
hα : NatTrans.Equifibered α
this :
  ∀ (x : C),
    Nonempty (IsColimit (((evaluation C D).obj x).mapCocone c')) ↔
      ∀ (j : J),
        IsPullback ((((evaluation C D).obj x).mapCocone c').ι.app j) ((whiskerRight α ((evaluation C D).obj x)).app j)
          (((evaluation C D).obj x).map f) ((((evaluation C D).obj x).mapCocone c).ι.app j)
hc' : IsColimit c'
j : J
x : C
⊢ IsLimit
    (PullbackCone.mk (((evaluation C D).obj x).map (c'.ι.app j)) (((evaluation C D).obj x).map (α.app j))
      (_ :
        ((evaluation C D).obj x).map (c'.ι.app j) ≫ ((evaluation C D).obj x).map f =
          ((evaluation C D).obj x).map (α.app j) ≫ ((evaluation C D).obj x).map (c.ι.app j)))
case mp.intro
J : Type v'
inst✝⁴ : Category J
C : Type u
inst✝³ : Category C
X Y : C
D : Type u''
inst✝² : Category D
inst✝¹ : HasPullbacks D
inst✝ : HasColimitsOfShape J D
F : J ⥤ C ⥤ D
c : Cocone F
hc : ∀ (x : C), IsVanKampenColimit (((evaluation C D).obj x).mapCocone c)
F' : J ⥤ C ⥤ D
c' : Cocone F'
α : F' ⟶ F
f : c'.pt ⟶ c.pt
e : α ≫ c.ι = c'.ι ≫ (Functor.const J).map f
hα : NatTrans.Equifibered α
this :
  ∀ (x : C),
    Nonempty (IsColimit (((evaluation C D).obj x).mapCocone c')) ↔
      ∀ (j : J),
        IsPullback ((((evaluation C D).obj x).mapCocone c').ι.app j) ((whiskerRight α ((evaluation C D).obj x)).app j)
          (((evaluation C D).obj x).map f) ((((evaluation C D).obj x).mapCocone c).ι.app j)
hc' : IsColimit c'
j : J
⊢ (k : C) →
    IsLimit
      (((evaluation C D).obj k).mapCone
        (PullbackCone.mk (c'.ι.app j) (α.app j) (_ : c'.ι.app j ≫ f = α.app j ≫ c.ι.app j)))
refine' fun x => (isLimitMapConePullbackConeEquiv _ _).symm _
no goals
case mp.intro
J : Type v'
inst✝⁴ : Category J
C : Type u
inst✝³ : Category C
X Y : C
D : Type u''
inst✝² : Category D
inst✝¹ : HasPullbacks D
inst✝ : HasColimitsOfShape J D
F : J ⥤ C ⥤ D
c : Cocone F
hc : ∀ (x : C), IsVanKampenColimit (((evaluation C D).obj x).mapCocone c)
F' : J ⥤ C ⥤ D
c' : Cocone F'
α : F' ⟶ F
f : c'.pt ⟶ c.pt
e : α ≫ c.ι = c'.ι ≫ (Functor.const J).map f
hα : NatTrans.Equifibered α
this :
  ∀ (x : C),
    Nonempty (IsColimit (((evaluation C D).obj x).mapCocone c')) ↔
      ∀ (j : J),
        IsPullback ((((evaluation C D).obj x).mapCocone c').ι.app j) ((whiskerRight α ((evaluation C D).obj x)).app j)
          (((evaluation C D).obj x).map f) ((((evaluation C D).obj x).mapCocone c).ι.app j)
hc' : IsColimit c'
j : J
x : C
⊢ IsLimit
    (PullbackCone.mk (((evaluation C D).obj x).map (c'.ι.app j)) (((evaluation C D).obj x).map (α.app j))
      (_ :
        ((evaluation C D).obj x).map (c'.ι.app j) ≫ ((evaluation C D).obj x).map f =
          ((evaluation C D).obj x).map (α.app j) ≫ ((evaluation C D).obj x).map (c.ι.app j)))
exact ((this x).mp ⟨PreservesColimit.preserves hc'⟩ _).isLimit
no goals
case mpr
J : Type v'
inst✝⁴ : Category J
C : Type u
inst✝³ : Category C
X Y : C
D : Type u''
inst✝² : Category D
inst✝¹ : HasPullbacks D
inst✝ : HasColimitsOfShape J D
F : J ⥤ C ⥤ D
c : Cocone F
hc : ∀ (x : C), IsVanKampenColimit (((evaluation C D).obj x).mapCocone c)
F' : J ⥤ C ⥤ D
c' : Cocone F'
α : F' ⟶ F
f : c'.pt ⟶ c.pt
e : α ≫ c.ι = c'.ι ≫ (Functor.const J).map f
hα : NatTrans.Equifibered α
this :
  ∀ (x : C),
    Nonempty (IsColimit (((evaluation C D).obj x).mapCocone c')) ↔
      ∀ (j : J),
        IsPullback ((((evaluation C D).obj x).mapCocone c').ι.app j) ((whiskerRight α ((evaluation C D).obj x)).app j)
          (((evaluation C D).obj x).map f) ((((evaluation C D).obj x).mapCocone c).ι.app j)
⊢ (∀ (j : J), IsPullback (c'.ι.app j) (α.app j) f (c.ι.app j)) → Nonempty (IsColimit c')
exact fun H => ⟨evaluationJointlyReflectsColimits _ fun x =>
  ((this x).mpr fun j => (H j).map ((evaluation C D).obj x)).some⟩