Merge pull request #21 from pitmonticone/golf

Golf
sinhp · Aug 29, 2024 · 61b872e · 61b872e
2 parents 1501769 + 3b7edbb
commit 61b872e
Show file tree

Hide file tree

Showing 2 changed files with 12 additions and 16 deletions.
diff --git a/GroupoidModel/Display.lean b/GroupoidModel/Display.lean
@@ -10,7 +10,6 @@ import GroupoidModel.NaturalModel
 
 -- (SH) TODO: Make the proof and construction work with `Disp` rather than `Disp'`.
 
-
 universe u
 
 open CategoryTheory Category Limits
@@ -35,7 +34,6 @@ structure Disp' where
   p : T ⟶ B
   disp : DisplayStruct π p := by infer_instance
 
-
 variable (C) in
 
 /-- `Cart C` is a typeclass synonym for `Arrow C` which comes equipped with
@@ -51,8 +49,8 @@ lemma IsPullback.of_horiz_id {X Y : C} (f : X ⟶ Y) : IsPullback (𝟙 X) f f (
 instance : Category (Cart C) where
   Hom p q := { v : p ⟶ q // IsPullback v.left p.hom q.hom v.right}
   id p := ⟨ ⟨𝟙 _, 𝟙 _, by simp⟩, IsPullback.of_horiz_id p.hom⟩
-  comp {p q r} u v := ⟨⟨u.1.left ≫ v.1.left, u.1.right ≫ v.1.right, by simp⟩, by
-    apply IsPullback.paste_horiz u.2 v.2⟩
+  comp {p q r} u v := ⟨⟨u.1.left ≫ v.1.left, u.1.right ≫ v.1.right, by simp⟩,
+    IsPullback.paste_horiz u.2 v.2⟩
   id_comp {p q} f:= by
     simp only [Functor.id_obj, Arrow.mk_left, Arrow.mk_right, id_comp]
     rfl -- we can replace by aesop, but they are a bit slow

diff --git a/GroupoidModel/Groupoids.lean b/GroupoidModel/Groupoids.lean
@@ -450,15 +450,15 @@ def GrothendieckLimisLim {Γ : Cat.{u,u}}(A : Γ ⥤ Cat.{u,u}) : Limits.IsLimit
   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 ⟨?_,?_,?_⟩
-  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)
+  · exact Grothendieck.UnivesalMap_CatVar'_Comm A s.pt FL (FR ⋙ (Down_uni Γ)) Comm
+  . rfl
+  · dsimp
+    intro 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
@@ -485,9 +485,7 @@ def Tm_functor : Grpd.{u,u}ᵒᵖ ⥤ Type (u + 1) where
 
 -- This is the typing natural transformation
 def tp_NatTrans : NatTrans Tm_functor Ty_functor where
-  app x := by
-    intro a
-    exact a ⋙ PGrpd.forgetPoint
+  app x := fun a ↦ a ⋙ PGrpd.forgetPoint
 
 -- This is the var construction of var before applying yoneda
 def var' (Γ : Grpd)(A : Γ ⥤ Grpd) : (GroupoidalGrothendieck A) ⥤ PGrpd where