From 5f3af25bec1c9ae32f130780617980b4b85a458d Mon Sep 17 00:00:00 2001
From: Spencer Woolfson <spencerwoolfson@Spencers-Laptop.local>
Date: Thu, 25 Jul 2024 00:13:32 -0400
Subject: [PATCH 1/2] working on pullbacks, right now everything is a mess.

---
 GroupoidModel/Groupoids.lean | 128 +++++++++++++++++++++++++++++++++++
 1 file changed, 128 insertions(+)

diff --git a/GroupoidModel/Groupoids.lean b/GroupoidModel/Groupoids.lean
index 9e0d3b8..a862b43 100644
--- a/GroupoidModel/Groupoids.lean
+++ b/GroupoidModel/Groupoids.lean
@@ -182,6 +182,16 @@ def PointedFunctor.comp {C : Type*}[PointedCategory C]{D : Type*}[PointedCategor
   toFunctor := F.toFunctor ⋙ G.toFunctor
   point := (G.map F.point) ≫ (G.point)
 
+theorem PointedFunctor.congr_func {C : Type*}[PointedCategory C]{D : Type*}[PointedCategory D]
+  {F G: PointedFunctor C D}(eq : F = G)  : F.toFunctor = G.toFunctor := congrArg toFunctor eq
+
+theorem PointedFunctor.congr_point {C : Type*}[pc :PointedCategory C]{D : Type*}[PointedCategory D]
+  (F G: PointedFunctor C D)(eq : F = G)  : F.point = (eqToHom (Functor.congr_obj (congr_func eq) pc.pt)) ≫ G.point := by
+    have h := (Functor.conj_eqToHom_iff_heq F.point G.point (Functor.congr_obj (congr_func eq) pc.pt) rfl).mpr
+    simp at h
+    apply h
+    rw[eq]
+
 /-- The category of pointed categorys and pointed functors-/
 def PCat.{w,z} :=
   Bundled PointedCategory.{w, z}
@@ -289,6 +299,124 @@ def var' (Γ : Grpd)(A : Γ ⥤ Grpd) : (GroupoidalGrothendieck A) ⥤ PGrpd whe
           ((Grpd.forgetToCat.map (A.map g.base)).obj
             ((Grpd.forgetToCat.map (A.map f.base)).obj X.fiber)))
 
+
+def Lift_dom {Γ : Type u}[Category.{u} Γ]{C : Type (u+1)}[Category.{u} C](A : Γ ⥤ C) : (ULift.{u+1,u} Γ) ⥤ C where
+  obj x := A.obj x.down
+  map f := A.map f
+  map_id x := by
+    simp[CategoryStruct.id]
+  map_comp f g := by
+    simp[CategoryStruct.comp]
+
+def Lift_domcod {Γ Δ: Type u}[Category.{u} Γ][Category.{u} Δ](F : Γ ⥤ Δ) : (ULift.{u+1,u} Γ) ⥤ (ULift.{u+1,u} Δ) where
+  obj x := {down := F.obj x.down}
+  map f := F.map f
+  map_id x := by
+    simp[CategoryStruct.id]
+  map_comp f g := by
+    simp[CategoryStruct.comp]
+
+def CastFunc {C : Cat.{u+1,u}}{F1 : C ⥤ Grpd.{u,u}}{F2 : C ⥤ Grpd.{u,u}}(Comm : F1 = F2 )(x : C) : Equivalence (F1.obj x) (F2.obj x) := by
+  have h := @Cat.equivOfIso (Grpd.forgetToCat.obj (F1.obj x)) (Grpd.forgetToCat.obj (F2.obj x)) (eqToIso (congrArg Grpd.forgetToCat.obj (Functor.congr_obj Comm x)))
+  dsimp[Grpd.forgetToCat,Cat.of,Bundled.of] at h
+  exact h
+
+def GrpdHelp (P : PGrpd.{u,u}) : P ⥤ (PGrpd.forgetPoint.obj P) := by
+  simp[PGrpd.forgetPoint]
+  exact Functor.id P
+
+def PB.vallift {Γ : Grpd.{u,u}}(A : Γ ⥤ Grpd.{u,u})(C : Cat.{u+1,u})(F1 : C ⥤ PGrpd.{u,u})(F2 : C ⥤ Γ)(Comm : F1 ⋙ PGrpd.forgetPoint = F2 ⋙ A) : C ⥤ GroupoidalGrothendieck A where
+  obj x := {base := (F2.obj x), fiber := ((GrpdHelp (F1.obj x)) ⋙ (CastFunc Comm x).functor).obj ((F1.obj x).str.pt)}
+  map f := by
+    rename_i X Y
+    refine {base := F2.map f, fiber := (eqToHom ?_) ≫ (((CastFunc Comm Y).functor).map (F1.map f).point)}
+    dsimp
+    have leftEQ : (Grpd.forgetToCat.map (A.map (F2.map f))).obj ((CastFunc Comm X).functor.obj ((GrpdHelp (F1.obj X)).obj (@PointedGroupoid.pt ((F1.obj X)) (F1.obj X).str))) =
+     ((GrpdHelp (F1.obj X)) ⋙ (CastFunc Comm X).functor ⋙ (Grpd.forgetToCat.map ((F2 ⋙ A).map f))).obj (@PointedGroupoid.pt (F1.obj X) (F1.obj X).str) := rfl
+    rw[leftEQ,(Functor.congr_hom Comm.symm f),Grpd.forgetToCat.map_comp,Grpd.forgetToCat.map_comp,eqToHom_map]
+    have eqToHomFunctorHelp : (CastFunc Comm X).functor ⋙ eqToHom (congr_arg Grpd.forgetToCat.obj (Functor.congr_obj (Eq.symm Comm) X)) = 𝟙 (Grpd.forgetToCat.obj (PGrpd.forgetPoint.obj (F1.obj X))) := by
+      have h : ∀ {X Y Z : Cat} (p : X = Y) (q : Y = Z), eqToHom p ≫ eqToHom q = eqToHom (p.trans q) := @eqToHom_trans Cat.{u,u} _
+      dsimp [CategoryStruct.comp] at h
+      simp [CastFunc,Cat.equivOfIso,h]
+    dsimp only [CategoryStruct.comp]
+    rw [<- Functor.assoc ((CastFunc Comm X).functor),eqToHomFunctorHelp]
+    simp [CategoryStruct.id]
+    aesop_cat
+  map_id x := by
+    simp[CategoryStruct.id,Grothendieck.id]
+    apply Grothendieck.ext
+    simp only [Grothendieck.Hom.fiber]
+    simp[(dcongr_arg PointedFunctor.point (F1.map_id x)),eqToHom_map,CategoryStruct.id]
+    exact F2.map_id x
+  map_comp f g := by
+    rename_i X Y Z
+    dsimp[CategoryStruct.comp,Grothendieck.comp]
+    apply Grothendieck.ext
+    have h := @PointedFunctor.congr_point (F1.obj X) _ (F1.obj Z) _ (F1.map (f ≫ g)) ((F1.map f)≫(F1.map g)) (F1.map_comp f g)
+    have h'' := (congrArg Grpd.forgetToCat.map (Functor.congr_hom Comm.symm g))
+    simp only [Functor.map_comp, eqToHom_map] at h''
+    have h' := Functor.congr_hom h'' ((CastFunc Comm Y).functor.map (F1.map f).point)
+    dsimp at h'
+    simp[Grothendieck.Hom.fiber,h,CategoryStruct.comp,eqToHom_map,h']
+    sorry
+    exact F2.map_comp f g
+
+abbrev LimDiag {Γ : Grpd.{u,u}}(A : Γ ⥤ Grpd.{u,u}) := (@CategoryTheory.Limits.PullbackCone Cat.{u,u+1} _ (Cat.of PGrpd.{u,u}) (Cat.of (ULift.{u+1,u} Γ)) (Cat.of Grpd.{u,u}) PGrpd.forgetPoint.{u,u} (Lift_dom A))
+
+def Lim {Γ : Grpd.{u,u}}(A : Γ ⥤ Grpd.{u,u}): (LimDiag A) where
+  pt := (Cat.of (ULift.{u+1,u} (GroupoidalGrothendieck A)))
+  π := by
+    constructor
+    case app;
+    intro X
+    cases X
+    case app.some;
+    rename_i X
+    cases X
+    dsimp
+    exact (Lift_dom (var' Γ A))
+    dsimp
+    exact (Lift_domcod GroupoidalGrothendieck.forget)
+    exact (Lift_domcod GroupoidalGrothendieck.forget) ⋙ (Lift_dom A)
+    intros X Y f
+    dsimp
+    cases f
+    simp
+    rename_i X
+    cases X
+    aesop_cat
+    aesop_cat
+
+
+def isLim {Γ : Grpd.{u,u}}(A : Γ ⥤ Grpd.{u,u}) : Limits.IsLimit (Lim A) := by
+  refine Limits.PullbackCone.isLimitAux' (Lim A) ?_
+  intro s
+  constructor
+  case val;
+  dsimp [Lim,Quiver.Hom,Cat.of,Bundled.of]
+  let FL := (s.π).app (Option.some Limits.WalkingPair.left)
+  let FR := (s.π).app (Option.some Limits.WalkingPair.right)
+  let FM := (s.π).app (Option.some Limits.WalkingPair.right)
+  dsimp [Quiver.Hom] at FL FR FM
+  let Comm := (s.π).naturality
+  sorry
+  dsimp
+  refine ⟨?_,?_,?_⟩
+  sorry
+  sorry
+  sorry
+
+
+theorem PB {Γ : Grpd.{u,u}}(A : Γ ⥤ Grpd.{u,u}): @IsPullback Cat.{u,u+1} _ (Cat.of (ULift.{u+1,u} (GroupoidalGrothendieck A))) (Cat.of PGrpd.{u,u}) (Cat.of (ULift.{u+1,u} Γ)) (Cat.of Grpd.{u,u}) (Lift_dom (var' Γ A)) (Lift_domcod GroupoidalGrothendieck.forget) PGrpd.forgetPoint (Lift_dom A) where
+  w := rfl
+  isLimit' := by
+    constructor
+    constructor
+    case val.lift;
+    intro s
+
+
+
 open GroupoidalGrothendieck
 
 -- Here I am useing sGrpd to be a small category version of Grpd. There is likely a better way to do this.

From 1769ee4169395dd38fa332107640b32ec038421a Mon Sep 17 00:00:00 2001
From: Spencer Woolfson <spencerwoolfson@Spencers-Laptop.local>
Date: Mon, 29 Jul 2024 08:52:41 -0400
Subject: [PATCH 2/2] Started work on pull backs

---
 GroupoidModel/Groupoids.lean | 354 ++++++++++++++++++++++-------------
 1 file changed, 222 insertions(+), 132 deletions(-)

diff --git a/GroupoidModel/Groupoids.lean b/GroupoidModel/Groupoids.lean
index a862b43..a15e7d0 100644
--- a/GroupoidModel/Groupoids.lean
+++ b/GroupoidModel/Groupoids.lean
@@ -165,7 +165,6 @@ def PointedCategory.of (C : Type*) (pt : C)[Category C]: PointedCategory C where
   pt := pt
 
 /-- The structure of a functor from C to D along with a morphism from the image of the point of C to the point of D -/
-@[ext]
 structure PointedFunctor (C : Type*)(D : Type*)[cp : PointedCategory C][dp : PointedCategory D] extends C ⥤ D where
   point : obj (cp.pt) ⟶ (dp.pt)
 
@@ -186,12 +185,30 @@ theorem PointedFunctor.congr_func {C : Type*}[PointedCategory C]{D : Type*}[Poin
   {F G: PointedFunctor C D}(eq : F = G)  : F.toFunctor = G.toFunctor := congrArg toFunctor eq
 
 theorem PointedFunctor.congr_point {C : Type*}[pc :PointedCategory C]{D : Type*}[PointedCategory D]
-  (F G: PointedFunctor C D)(eq : F = G)  : F.point = (eqToHom (Functor.congr_obj (congr_func eq) pc.pt)) ≫ G.point := by
+  {F G: PointedFunctor C D}(eq : F = G)  : F.point = (eqToHom (Functor.congr_obj (congr_func eq) pc.pt)) ≫ G.point := by
     have h := (Functor.conj_eqToHom_iff_heq F.point G.point (Functor.congr_obj (congr_func eq) pc.pt) rfl).mpr
     simp at h
     apply h
     rw[eq]
 
+@[ext]
+theorem PointedFunctor.ext {C : Type*}[pc :PointedCategory C]{D : Type*}[PointedCategory D]
+  (F G: PointedFunctor C D)(h_func : F.toFunctor = G.toFunctor)(h_point : F.point = (eqToHom (Functor.congr_obj h_func pc.pt)) ≫ G.point) : F = G := by
+  rcases F with ⟨F.func,F.point⟩
+  rcases G with ⟨G.func,G.point⟩
+  congr
+  simp at h_point
+  have temp : G.point = G.point ≫ (eqToHom rfl) := by simp
+  rw [temp] at h_point
+  exact
+    (Functor.conj_eqToHom_iff_heq F.point G.point
+          (congrFun (congrArg Prefunctor.obj (congrArg Functor.toPrefunctor h_func))
+            PointedCategory.pt)
+          rfl).mp
+      h_point
+
+
+
 /-- The category of pointed categorys and pointed functors-/
 def PCat.{w,z} :=
   Bundled PointedCategory.{w, z}
@@ -212,6 +229,20 @@ instance category : LargeCategory.{max v u} PCat.{v, u} where
   Hom C D := PointedFunctor C D
   id C := PointedFunctor.id C
   comp f g := PointedFunctor.comp f g
+  comp_id f := by
+    apply PointedFunctor.ext
+    simp
+    simp [PointedFunctor.id,PointedFunctor.comp,Functor.comp_id]
+  id_comp f := by
+    apply PointedFunctor.ext
+    simp
+    simp [PointedFunctor.id,PointedFunctor.comp,Functor.id_comp]
+  assoc f g h := by
+    apply PointedFunctor.ext
+    simp
+    simp [PointedFunctor.comp,Functor.assoc]
+
+
 
 /-- The functor that takes PCat to Cat by forgeting the points-/
 def forgetPoint : PCat ⥤ Cat where
@@ -247,6 +278,18 @@ instance category : LargeCategory.{max v u} PGrpd.{v, u} where
   Hom C D := PointedFunctor C D
   id C := PointedFunctor.id C
   comp f g := PointedFunctor.comp f g
+  comp_id f := by
+    apply PointedFunctor.ext
+    simp
+    simp [PointedFunctor.id,PointedFunctor.comp,Functor.comp_id]
+  id_comp f := by
+    apply PointedFunctor.ext
+    simp
+    simp [PointedFunctor.id,PointedFunctor.comp,Functor.id_comp]
+  assoc f g h := by
+    apply PointedFunctor.ext
+    simp
+    simp [PointedFunctor.comp,Functor.assoc]
 
 /-- The functor that takes PGrpd to Grpd by forgeting the points-/
 def forgetPoint : PGrpd ⥤ Grpd where
@@ -257,165 +300,212 @@ end PGrpd
 
 end PointedCategorys
 
-section NaturalModelBase
-
--- This is a Covariant Functor that takes a Groupoid Γ to Γ ⥤ Grpd
-def Ty_functor : Grpd.{u,u}ᵒᵖ ⥤ Type (u + 1) where
-  obj x := x.unop ⥤ Grpd.{u,u}
-  map f A := f.unop ⋙ A
-
--- This is a Covariant Functor that takes a Groupoid Γ to Γ ⥤ PointedGroupoid
-def Tm_functor : Grpd.{u,u}ᵒᵖ ⥤ Type (u + 1) where
-  obj x := x.unop ⥤ PGrpd.{u,u}
-  map f A := f.unop ⋙ A
+section Pullbacks
+/-
+In this section we prove that the following square is a PullBack
+
+  Grothendieck A --- CatVar' ----> PCat
+        |                           |
+        |                           |
+ Grothendieck.forget        PCat.forgetPoint
+        |                           |
+        v                           v
+        Γ-------------A----------->Cat
+-/
 
--- This is the typing natral transformation
-def tp_NatTrans : NatTrans Tm_functor Ty_functor where
-  app x := by
-    intro a
-    exact a ⋙ PGrpd.forgetPoint
 
--- This is the var construction of var before applying yoneda
-def var' (Γ : Grpd)(A : Γ ⥤ Grpd) : (GroupoidalGrothendieck A) ⥤ PGrpd where
-  obj x := ⟨(A.obj x.base), (PointedGroupoid.of (A.obj x.base) x.fiber)⟩
+-- This takes in two equal functors F and G from C in to Cat and an x:C and returns (F.obj x) ≅ (G.obj x).
+def CastFunc {C : Cat.{u,u+1}}{F1 : C ⥤ Cat.{u,u}}{F2 : C ⥤ Cat.{u,u}}(Comm : F1 = F2 )(x : C) : Equivalence (F1.obj x) (F2.obj x) := Cat.equivOfIso (eqToIso (Functor.congr_obj  Comm  x))
+
+-- This is a functor that takes a category up a universe level
+def Up_uni (Δ : Type u)[Category.{u} Δ] :  Δ ⥤ (ULift.{u+1,u} Δ) where
+  obj x := {down := x}
+  map f := f
+
+-- This is a functor that takes a category down a universe level
+def Down_uni (Δ : Type u)[Category.{u} Δ]: (ULift.{u+1,u} Δ) ⥤ Δ where
+  obj x := x.down
+  map f := f
+
+-- This is a helper theorem for eliminating Up_uni and Down_uni functors
+theorem Up_Down {C : Type (u+1)}[Category.{u} C]{Δ : Type u}[Category.{u} Δ] (F : C ⥤ Δ) (G : C ⥤ (ULift.{u+1,u} Δ)): ((F ⋙ (Up_uni Δ)) = G) ↔ (F = (G ⋙ (Down_uni Δ))) := by
+  unfold Up_uni
+  unfold Down_uni
+  simp [Functor.comp]
+  refine Iff.intro ?_ ?_
+  intro h
+  rw[<- h]
+  intro h
+  rw[h]
+
+-- This is the functor from the Grothendieck to Pointed Categorys
+def CatVar' (Γ : Cat)(A : Γ ⥤ Cat) : (Grothendieck A) ⥤ PCat where
+  obj x := ⟨(A.obj x.base), PointedCategory.of (A.obj x.base) x.fiber⟩
   map f := ⟨A.map f.base, f.fiber⟩
   map_id x := by
-    dsimp [CategoryStruct.id]
-    congr 1
-    · simp only [A.map_id]; rfl
-    · exact cast_heq (Eq.symm (eqToHom.proof_1 (Grothendieck.id.proof_1 x))) (𝟙 x.fiber)
-  map_comp {X Y Z} f g := by
-    dsimp [CategoryStruct.comp,PointedFunctor.comp]
-    congr 1
-    exact A.map_comp f.base g.base
-    dsimp [eqToHom]
-    have h := (Category.id_comp ((A.map g.base).map f.fiber ≫ g.fiber))
-    rw [← h]
-    congr 1
-    simp [Grpd.forgetToCat, CategoryStruct.comp]
-    exact
-      cast_heq (Eq.symm (eqToHom.proof_1 (Grothendieck.comp.proof_1 f g)))
-        (𝟙
-          ((Grpd.forgetToCat.map (A.map g.base)).obj
-            ((Grpd.forgetToCat.map (A.map f.base)).obj X.fiber)))
-
-
-def Lift_dom {Γ : Type u}[Category.{u} Γ]{C : Type (u+1)}[Category.{u} C](A : Γ ⥤ C) : (ULift.{u+1,u} Γ) ⥤ C where
-  obj x := A.obj x.down
-  map f := A.map f
-  map_id x := by
-    simp[CategoryStruct.id]
-  map_comp f g := by
-    simp[CategoryStruct.comp]
-
-def Lift_domcod {Γ Δ: Type u}[Category.{u} Γ][Category.{u} Δ](F : Γ ⥤ Δ) : (ULift.{u+1,u} Γ) ⥤ (ULift.{u+1,u} Δ) where
-  obj x := {down := F.obj x.down}
-  map f := F.map f
-  map_id x := by
+    dsimp
+    let _ := (PointedCategory.of (A.obj x.base) x.fiber)
+    apply PointedFunctor.ext
     simp[CategoryStruct.id]
-  map_comp f g := by
-    simp[CategoryStruct.comp]
+    simp[CategoryStruct.id,PointedFunctor.id]
+  map_comp {x y z} f g := by
+    dsimp [CategoryStruct.comp,PointedFunctor.comp]
+    let _ := (PointedCategory.of (A.obj x.base) x.fiber)
+    let _ := (PointedCategory.of (A.obj z.base) z.fiber)
+    apply PointedFunctor.ext
+    simp
+    simp[A.map_comp,CategoryStruct.comp]
 
-def CastFunc {C : Cat.{u+1,u}}{F1 : C ⥤ Grpd.{u,u}}{F2 : C ⥤ Grpd.{u,u}}(Comm : F1 = F2 )(x : C) : Equivalence (F1.obj x) (F2.obj x) := by
-  have h := @Cat.equivOfIso (Grpd.forgetToCat.obj (F1.obj x)) (Grpd.forgetToCat.obj (F2.obj x)) (eqToIso (congrArg Grpd.forgetToCat.obj (Functor.congr_obj Comm x)))
-  dsimp[Grpd.forgetToCat,Cat.of,Bundled.of] at h
-  exact h
+-- This is the proof that the square commutes
+theorem Comm {Γ : Cat}(A : Γ ⥤ Cat) : (Down_uni (Grothendieck A) ⋙ CatVar' Γ A) ⋙ PCat.forgetPoint =
+  ((Down_uni (Grothendieck A)) ⋙ Grothendieck.forget A ⋙ (Up_uni Γ)) ⋙ Down_uni ↑Γ ⋙ A := by
+    apply Functor.ext
+    intros X Y f
+    simp [PCat.forgetPoint,Down_uni,Up_uni,CatVar']
+    intro X
+    simp [PCat.forgetPoint,Down_uni,Up_uni,CatVar']
+    exact rfl
 
-def GrpdHelp (P : PGrpd.{u,u}) : P ⥤ (PGrpd.forgetPoint.obj P) := by
-  simp[PGrpd.forgetPoint]
+-- This is a helper functor from from a pointed category to itself without a point
+def ForgetPointFunctor (P : PCat.{u,u}) : P ⥤ (PCat.forgetPoint.obj P) := by
+  simp[PCat.forgetPoint]
   exact Functor.id P
 
-def PB.vallift {Γ : Grpd.{u,u}}(A : Γ ⥤ Grpd.{u,u})(C : Cat.{u+1,u})(F1 : C ⥤ PGrpd.{u,u})(F2 : C ⥤ Γ)(Comm : F1 ⋙ PGrpd.forgetPoint = F2 ⋙ A) : C ⥤ GroupoidalGrothendieck A where
-  obj x := {base := (F2.obj x), fiber := ((GrpdHelp (F1.obj x)) ⋙ (CastFunc Comm x).functor).obj ((F1.obj x).str.pt)}
+-- This is the construction of universal map of th limit
+def Grothendieck.UnivesalMap {Γ : Cat.{u,u}}(A : Γ ⥤ Cat.{u,u})(C : Cat.{u,u+1})
+  (F1 : C ⥤ PCat.{u,u})(F2 : C ⥤ Γ)(Comm : F1 ⋙ PCat.forgetPoint = F2 ⋙ A) : C ⥤ Grothendieck A where
+  obj x := {base := (F2.obj x), fiber := ((ForgetPointFunctor (F1.obj x)) ⋙ (CastFunc Comm x).functor).obj ((F1.obj x).str.pt)}
   map f := by
     rename_i X Y
     refine {base := F2.map f, fiber := (eqToHom ?_) ≫ (((CastFunc Comm Y).functor).map (F1.map f).point)}
     dsimp
-    have leftEQ : (Grpd.forgetToCat.map (A.map (F2.map f))).obj ((CastFunc Comm X).functor.obj ((GrpdHelp (F1.obj X)).obj (@PointedGroupoid.pt ((F1.obj X)) (F1.obj X).str))) =
-     ((GrpdHelp (F1.obj X)) ⋙ (CastFunc Comm X).functor ⋙ (Grpd.forgetToCat.map ((F2 ⋙ A).map f))).obj (@PointedGroupoid.pt (F1.obj X) (F1.obj X).str) := rfl
-    rw[leftEQ,(Functor.congr_hom Comm.symm f),Grpd.forgetToCat.map_comp,Grpd.forgetToCat.map_comp,eqToHom_map]
-    have eqToHomFunctorHelp : (CastFunc Comm X).functor ⋙ eqToHom (congr_arg Grpd.forgetToCat.obj (Functor.congr_obj (Eq.symm Comm) X)) = 𝟙 (Grpd.forgetToCat.obj (PGrpd.forgetPoint.obj (F1.obj X))) := by
-      have h : ∀ {X Y Z : Cat} (p : X = Y) (q : Y = Z), eqToHom p ≫ eqToHom q = eqToHom (p.trans q) := @eqToHom_trans Cat.{u,u} _
-      dsimp [CategoryStruct.comp] at h
-      simp [CastFunc,Cat.equivOfIso,h]
-    dsimp only [CategoryStruct.comp]
-    rw [<- Functor.assoc ((CastFunc Comm X).functor),eqToHomFunctorHelp]
-    simp [CategoryStruct.id]
-    aesop_cat
+    have h1 := Functor.congr_hom Comm.symm f
+    dsimp at h1
+    have h2 : (eqToHom (Functor.congr_obj (Eq.symm Comm) X)).obj
+     ((eqToHom (CastFunc.proof_1 Comm X )).obj (@PointedCategory.pt (↑(F1.obj X)) (F1.obj X).str)) =
+      ((eqToHom (CastFunc.proof_1 Comm X)) ≫ (eqToHom (Functor.congr_obj (Eq.symm Comm) X))).obj
+       (@PointedCategory.pt (↑(F1.obj X)) (F1.obj X).str) := by rfl
+    simp[h1,CastFunc,Cat.equivOfIso,ForgetPointFunctor,h2,eqToHom_trans,eqToHom_refl,CategoryStruct.id,PCat.forgetPoint]
   map_id x := by
-    simp[CategoryStruct.id,Grothendieck.id]
+    dsimp [CategoryStruct.id,Grothendieck.id]
     apply Grothendieck.ext
-    simp only [Grothendieck.Hom.fiber]
-    simp[(dcongr_arg PointedFunctor.point (F1.map_id x)),eqToHom_map,CategoryStruct.id]
+    simp[Grothendieck.Hom.fiber,(dcongr_arg PointedFunctor.point (F1.map_id x)),eqToHom_map,CategoryStruct.id]
     exact F2.map_id x
   map_comp f g := by
-    rename_i X Y Z
-    dsimp[CategoryStruct.comp,Grothendieck.comp]
-    apply Grothendieck.ext
-    have h := @PointedFunctor.congr_point (F1.obj X) _ (F1.obj Z) _ (F1.map (f ≫ g)) ((F1.map f)≫(F1.map g)) (F1.map_comp f g)
-    have h'' := (congrArg Grpd.forgetToCat.map (Functor.congr_hom Comm.symm g))
-    simp only [Functor.map_comp, eqToHom_map] at h''
-    have h' := Functor.congr_hom h'' ((CastFunc Comm Y).functor.map (F1.map f).point)
-    dsimp at h'
-    simp[Grothendieck.Hom.fiber,h,CategoryStruct.comp,eqToHom_map,h']
     sorry
-    exact F2.map_comp f g
-
-abbrev LimDiag {Γ : Grpd.{u,u}}(A : Γ ⥤ Grpd.{u,u}) := (@CategoryTheory.Limits.PullbackCone Cat.{u,u+1} _ (Cat.of PGrpd.{u,u}) (Cat.of (ULift.{u+1,u} Γ)) (Cat.of Grpd.{u,u}) PGrpd.forgetPoint.{u,u} (Lift_dom A))
 
-def Lim {Γ : Grpd.{u,u}}(A : Γ ⥤ Grpd.{u,u}): (LimDiag A) where
-  pt := (Cat.of (ULift.{u+1,u} (GroupoidalGrothendieck A)))
-  π := by
-    constructor
-    case app;
-    intro X
-    cases X
-    case app.some;
-    rename_i X
-    cases X
-    dsimp
-    exact (Lift_dom (var' Γ A))
-    dsimp
-    exact (Lift_domcod GroupoidalGrothendieck.forget)
-    exact (Lift_domcod GroupoidalGrothendieck.forget) ⋙ (Lift_dom A)
-    intros X Y f
-    dsimp
-    cases f
-    simp
-    rename_i X
-    cases X
-    aesop_cat
-    aesop_cat
+--This is the proof that the universal map composed with CatVar' is the the map F1
+theorem Grothendieck.UnivesalMap_CatVar'_Comm {Γ : Cat.{u,u}}(A : Γ ⥤ Cat.{u,u})(C : Cat.{u,u+1})
+  (F1 : C ⥤ PCat.{u,u})(F2 : C ⥤ Γ)(Comm : F1 ⋙ PCat.forgetPoint = F2 ⋙ A) : (Grothendieck.UnivesalMap A C F1 F2 Comm) ⋙ (CatVar' Γ A) = F1 := by
+    apply Functor.ext
+    case h_obj;
+    intro x
+    have Comm' := Functor.congr_obj Comm x
+    simp [PCat.forgetPoint] at Comm'
+    simp [UnivesalMap,CatVar']
+    congr 1
+    simp [<- Comm',Cat.of,Bundled.of]
+    simp [PointedCategory.of,ForgetPointFunctor,CastFunc,Cat.equivOfIso]
+    sorry
+    sorry
 
+-- This is the proof that the universal map is unique
+theorem Grothendieck.UnivesalMap_Uniq {Γ : Cat.{u,u}}(A : Γ ⥤ Cat.{u,u})(C : Cat.{u,u+1})
+  (F1 : C ⥤ PCat.{u,u})(F2 : C ⥤ Γ)(Comm : F1 ⋙ PCat.forgetPoint = F2 ⋙ A)(F : C ⥤ Grothendieck A)
+  (F1comm :F ⋙ (CatVar' Γ A) = F1)(F2comm : F ⋙ (Grothendieck.forget A) = F2)  : F = (Grothendieck.UnivesalMap A C F1 F2 Comm) := by
+    sorry
 
-def isLim {Γ : Grpd.{u,u}}(A : Γ ⥤ Grpd.{u,u}) : Limits.IsLimit (Lim A) := by
-  refine Limits.PullbackCone.isLimitAux' (Lim A) ?_
+-- This is the type of cones
+abbrev GrothendieckCones {Γ : Cat.{u,u}}(A : Γ ⥤ Cat.{u,u}) := @CategoryTheory.Limits.PullbackCone Cat.{u,u+1} _
+  (Cat.of.{u,u+1} PCat.{u,u})
+  (Cat.of.{u,u+1} (ULift.{u+1,u} Γ))
+  (Cat.of.{u,u+1} Cat.{u,u})
+  PCat.forgetPoint.{u,u}
+  ((Down_uni Γ) ⋙ A)
+
+-- This is the cone we will prove is the limit
+abbrev GrothendieckLim {Γ : Cat.{u,u}}(A : Γ ⥤ Cat.{u,u}): (GrothendieckCones A) :=
+  @Limits.PullbackCone.mk Cat.{u,u+1} _
+    (Cat.of PCat.{u,u})
+    (Cat.of (ULift.{u + 1, u} Γ))
+    (Cat.of Cat.{u,u})
+    (PCat.forgetPoint.{u,u})
+    ((Down_uni Γ) ⋙ A)
+    (Cat.of (ULift.{u+1,u} (Grothendieck A)))
+    ((Down_uni (Grothendieck A)) ⋙ CatVar' Γ A)
+    (Down_uni (Grothendieck A) ⋙ Grothendieck.forget A ⋙ Up_uni Γ)
+    (Comm A)
+
+-- This is the proof that the limit cone iis a limit
+def GrothendieckLimisLim {Γ : Cat.{u,u}}(A : Γ ⥤ Cat.{u,u}) : Limits.IsLimit (GrothendieckLim A) := by
+  refine Limits.PullbackCone.isLimitAux' (GrothendieckLim A) ?_
   intro s
-  constructor
-  case val;
-  dsimp [Lim,Quiver.Hom,Cat.of,Bundled.of]
   let FL := (s.π).app (Option.some Limits.WalkingPair.left)
   let FR := (s.π).app (Option.some Limits.WalkingPair.right)
-  let FM := (s.π).app (Option.some Limits.WalkingPair.right)
-  dsimp [Quiver.Hom] at FL FR FM
-  let Comm := (s.π).naturality
-  sorry
-  dsimp
+  let Comm := (((s.π).naturality (Limits.WalkingCospan.Hom.inl)).symm).trans ((s.π).naturality (Limits.WalkingCospan.Hom.inr))
+  dsimp [Quiver.Hom] at FL FR Comm
+  constructor
+  case val;
+  dsimp [GrothendieckLim,Quiver.Hom,Cat.of,Bundled.of]
+  refine (Grothendieck.UnivesalMap A s.pt FL (FR ⋙ (Down_uni Γ)) ?_) ⋙ (Up_uni (Grothendieck A))
+  exact (((s.π).naturality (Limits.WalkingCospan.Hom.inl)).symm).trans ((s.π).naturality (Limits.WalkingCospan.Hom.inr))
   refine ⟨?_,?_,?_⟩
-  sorry
-  sorry
-  sorry
+  exact Grothendieck.UnivesalMap_CatVar'_Comm A s.pt FL (FR ⋙ (Down_uni Γ)) Comm
+  exact rfl
+  dsimp
+  intros m h1 h2
+  have r := Grothendieck.UnivesalMap_Uniq A s.pt FL (FR ⋙ (Down_uni Γ)) Comm (m ⋙ (Down_uni (Grothendieck A))) h1 ?C
+  exact ((Up_Down (Grothendieck.UnivesalMap A s.pt FL (FR ⋙ Down_uni ↑Γ) Comm) m).mpr r.symm).symm
+  dsimp [CategoryStruct.comp] at h2
+  rw [<- Functor.assoc,<- Functor.assoc] at h2
+  exact ((Up_Down (((m ⋙ Down_uni (Grothendieck A)) ⋙ Grothendieck.forget A)) s.snd).mp h2)
+
+-- This converts the proof of the limit to the proof of a pull back
+theorem GrothendieckLimisPullBack {Γ : Cat.{u,u}}(A : Γ ⥤ Cat.{u,u}) : @IsPullback (Cat.{u,u+1}) _ (Cat.of (ULift.{u+1,u} (Grothendieck A))) (Cat.of PCat.{u,u}) (Cat.of (ULift.{u+1,u} Γ)) (Cat.of Cat.{u,u}) ((Down_uni (Grothendieck A)) ⋙ (CatVar' Γ A)) ((Down_uni (Grothendieck A)) ⋙ (Grothendieck.forget A) ⋙ (Up_uni Γ)) (PCat.forgetPoint) ((Down_uni Γ) ⋙ A) := by
+  constructor
+  case toCommSq;
+    constructor;
+    exact Comm A;
+  constructor
+  exact GrothendieckLimisLim A
 
+end Pullbacks
 
-theorem PB {Γ : Grpd.{u,u}}(A : Γ ⥤ Grpd.{u,u}): @IsPullback Cat.{u,u+1} _ (Cat.of (ULift.{u+1,u} (GroupoidalGrothendieck A))) (Cat.of PGrpd.{u,u}) (Cat.of (ULift.{u+1,u} Γ)) (Cat.of Grpd.{u,u}) (Lift_dom (var' Γ A)) (Lift_domcod GroupoidalGrothendieck.forget) PGrpd.forgetPoint (Lift_dom A) where
-  w := rfl
-  isLimit' := by
-    constructor
-    constructor
-    case val.lift;
-    intro s
+section NaturalModelBase
+
+-- This is a Covariant Functor that takes a Groupoid Γ to Γ ⥤ Grpd
+def Ty_functor : Grpd.{u,u}ᵒᵖ ⥤ Type (u + 1) where
+  obj x := x.unop ⥤ Grpd.{u,u}
+  map f A := f.unop ⋙ A
 
+-- This is a Covariant Functor that takes a Groupoid Γ to Γ ⥤ PointedGroupoid
+def Tm_functor : Grpd.{u,u}ᵒᵖ ⥤ Type (u + 1) where
+  obj x := x.unop ⥤ PGrpd.{u,u}
+  map f A := f.unop ⋙ A
+
+-- This is the typing natral transformation
+def tp_NatTrans : NatTrans Tm_functor Ty_functor where
+  app x := by
+    intro a
+    exact a ⋙ PGrpd.forgetPoint
 
+-- This is the var construction of var before applying yoneda
+def var' (Γ : Grpd)(A : Γ ⥤ Grpd) : (GroupoidalGrothendieck A) ⥤ PGrpd where
+  obj x := ⟨(A.obj x.base), (PointedGroupoid.of (A.obj x.base) x.fiber)⟩
+  map f := ⟨A.map f.base, f.fiber⟩
+  map_id x := by
+    dsimp
+    let _ := (PointedCategory.of (A.obj x.base) x.fiber)
+    apply PointedFunctor.ext
+    simp[CategoryStruct.id]
+    simp[CategoryStruct.id,PointedFunctor.id]
+  map_comp {x y z} f g := by
+    dsimp [CategoryStruct.comp,PointedFunctor.comp]
+    let _ := (PointedCategory.of (A.obj x.base) x.fiber)
+    let _ := (PointedCategory.of (A.obj z.base) z.fiber)
+    apply PointedFunctor.ext
+    simp [Grpd.forgetToCat]
+    simp[A.map_comp,CategoryStruct.comp]
 
 open GroupoidalGrothendieck