feat: Structured model

HoTTLean.lean

@@ -2,4 +2,5 @@ import HoTTLean.Groupoids.Sigma
 import HoTTLean.Groupoids.Pi
 import HoTTLean.Groupoids.Id
 import HoTTLean.Model.Unstructured.Interpretation
+import HoTTLean.Model.Structured.StructuredUniverse
 import HoTTLean.Frontend.Commands

HoTTLean/ForMathlib.lean

@@ -538,30 +538,6 @@ variable {C : Type u₁} [SmallCategory C] {F G : Cᵒᵖ ⥤ Type u₁}
   (naturality : ∀ {X Y : C} (f : X ⟶ Y) (α : yoneda.obj Y ⟶ F),
     app (yoneda.map f ≫ α) = yoneda.map f ≫ app α)
 
-variable (F) in
-/--
-  A presheaf `F` on a small category `C` is isomorphic to
-  the hom-presheaf `Hom(y(•),F)`.
--/
-def yonedaIso : yoneda.op ⋙ yoneda.obj F ≅ F :=
-  NatIso.ofComponents (fun _ => Equiv.toIso yonedaEquiv)
-    (fun f => by ext : 1; dsimp; rw [yonedaEquiv_naturality'])
-
-def yonedaIsoMap : yoneda.op ⋙ yoneda.obj F ⟶ yoneda.op ⋙ yoneda.obj G where
-  app _ := app
-  naturality _ _ _ := by ext : 1; apply naturality
-
-/-- Build natural transformations between presheaves on a small category
-  by defining their action when precomposing by a morphism with
-  representable domain -/
-def NatTrans.yonedaMk : F ⟶ G :=
-  (yonedaIso F).inv ≫ yonedaIsoMap app naturality ≫ (yonedaIso G).hom
-
-theorem NatTrans.yonedaMk_app {X : C} (α : yoneda.obj X ⟶ F) :
-    α ≫ yonedaMk app naturality = app α := by
-  rw [← yonedaEquiv.apply_eq_iff_eq, yonedaEquiv_comp]
-  simp [yonedaMk, yonedaIso, yonedaIsoMap]
-
 namespace Functor
 
 theorem precomp_heq_of_heq_id {A B : Type u} {C : Type*} [Category.{v} A] [Category.{v} B] [Category C]
@@ -624,14 +600,6 @@ lemma Discrete.functor_eq {X C : Type*} [Category C] {F : Discrete X ⥤ C} :
     cases h
     simp
 
-lemma Discrete.functor_ext {X C : Type*} [Category C] (F G : Discrete X ⥤ C)
-    (h : ∀ x : X, F.obj ⟨x⟩ = G.obj ⟨x⟩) :
-    F = G :=
-  calc F
-    _ = Discrete.functor (fun x => F.obj ⟨x⟩) := Discrete.functor_eq
-    _ = Discrete.functor (fun x => G.obj ⟨x⟩) := Discrete.functor_ext' h
-    _ = G := Discrete.functor_eq.symm
-
 lemma Discrete.hext {X Y : Type u} (a : Discrete X) (b : Discrete Y) (hXY : X ≍ Y)
     (hab : a.1 ≍ b.1) : a ≍ b := by
   aesop_cat

HoTTLean/ForMathlib/CategoryTheory/Adjunction/Basic.lean

@@ -0,0 +1,49 @@
+import Mathlib.CategoryTheory.Adjunction.Basic
+
+namespace CategoryTheory
+
+open CategoryTheory.Functor NatIso Category
+
+-- declare the `v`'s first; see `CategoryTheory.Category` for an explanation
+universe v₁ v₂ v₃ u₁ u₂ u₃
+variable {C : Type u₁} [Category.{v₁} C] {D : Type u₂}
+
+/-- The natural hom-set isomorphism `C(F(-),⋆) ≅ D(-,G(⋆))` given by an adjunction. -/
+def Adjunction.homIso [Category.{v₁} D] {F : C ⥤ D} {G : D ⥤ C} (adj : F ⊣ G) :
+    yoneda ⋙ (Functor.whiskeringLeft _ _ _).obj (F.op) ≅ G ⋙ yoneda :=
+  NatIso.ofComponents
+  (fun X => (adj.representableBy X).toIso.symm)
+  (fun {X Y} f => by ext; simp [Functor.RepresentableBy.toIso, Functor.representableByEquiv,
+    adj.homEquiv_naturality_right])
+
+namespace Equivalence
+
+variable [Category.{v₂} D] {e : C ≌ D}
+
+def isoCompInverse {J : Type*} [Category J] {X : J ⥤ C} {Y : J ⥤ D} (α : X ⋙ e.functor ≅ Y) :
+    X ≅ Y ⋙ e.inverse :=
+  calc X
+  _ ≅ X ⋙ 𝟭 _ := X.rightUnitor.symm
+  _ ≅ X ⋙ e.functor ⋙ e.inverse := Functor.isoWhiskerLeft X e.unitIso
+  _ ≅ (X ⋙ e.functor) ⋙ e.inverse := Functor.associator ..
+  _ ≅ Y ⋙ e.inverse := Functor.isoWhiskerRight α e.inverse
+
+@[simp]
+lemma isoCompInverse_hom_app {J : Type*} [Category J] {X : J ⥤ C} {Y : J ⥤ D}
+    (α : X ⋙ e.functor ≅ Y) (A : J) :
+    (isoCompInverse α).hom.app A = e.unitIso.hom.app (X.obj A) ≫ e.inverse.map (α.hom.app A) := by
+  simp [isoCompInverse, Trans.trans]
+
+@[simp]
+lemma isoCompInverse_inv_app {J : Type*} [Category J] {X : J ⥤ C} {Y : J ⥤ D}
+    (α : X ⋙ e.functor ≅ Y) (A : J) :
+    (isoCompInverse α).inv.app A = e.inverse.map (α.inv.app A) ≫ e.unitIso.inv.app (X.obj A) := by
+  simp [isoCompInverse, Trans.trans]
+
+@[simps]
+def compFunctorNatIsoEquiv {J : Type*} [Category J] (X : J ⥤ C) (Y : J ⥤ D) :
+    (X ⋙ e.functor ≅ Y) ≃ (X ≅ Y ⋙ e.inverse) where
+  toFun := isoCompInverse
+  invFun α := (e.symm.isoCompInverse α.symm).symm
+  left_inv := by cat_disch
+  right_inv := by cat_disch

HoTTLean/ForMathlib/CategoryTheory/Adjunction/PartialAdjoint.lean

@@ -0,0 +1,66 @@
+import Mathlib.CategoryTheory.Adjunction.PartialAdjoint
+
+
+universe v₁ v₂ u₁ u₂
+
+namespace CategoryTheory
+
+namespace Functor
+
+open Category Opposite Limits
+
+section PartialRightAdjoint
+
+variable {C : Type u₁} [Category.{v₁} C] {D : Type u₂} [Category.{v₂} D] (F : C ⥤ D)
+
+structure PartialRightAdjoint (G : F.PartialRightAdjointSource ⥤ C) where
+  (repr : ∀ Y, (F.op ⋙ yoneda.obj Y.obj).RepresentableBy (G.obj Y))
+  (repr_homEquiv : ∀ X Y (f : X ⟶ Y), (repr Y).homEquiv (G.map f) =
+    (repr X).homEquiv (𝟙 _) ≫ f)
+
+@[simps]
+noncomputable def PartialRightAdjoint.partialRightAdjoint :
+    PartialRightAdjoint F (partialRightAdjoint F) where
+  repr _ := Functor.representableBy _
+  repr_homEquiv _ _ _ := by
+    simp only [partialRightAdjoint_obj, comp_obj, op_obj, yoneda_obj_obj, partialRightAdjoint_map,
+      partialRightAdjointMap, partialRightAdjointHomEquiv]
+    erw [Equiv.apply_symm_apply]
+
+@[simps]
+noncomputable def rightAdjoint.partialRightAdjoint (L : C ⥤ D) [IsLeftAdjoint L] :
+    PartialRightAdjoint L (ObjectProperty.ι _ ⋙ rightAdjoint L) where
+  repr Y := Adjunction.representableBy (Adjunction.ofIsLeftAdjoint L) _
+  repr_homEquiv a b c := by
+    simp [Equiv.symm_apply_eq, Adjunction.homEquiv_naturality_right]
+
+lemma PartialRightAdjoint.repr_homEquiv_comp {G : F.PartialRightAdjointSource ⥤ C}
+    (P : PartialRightAdjoint F G) {X Y Z} (f : X ⟶ Y) (a : Z ⟶ G.obj X) :
+    (P.repr Y).homEquiv (a ≫ G.map f) = (P.repr X).homEquiv a ≫ f := by
+  have := (P.repr X).homEquiv_comp a (𝟙 _)
+  rw [(P.repr Y).homEquiv_comp, P.repr_homEquiv]
+  cat_disch
+
+lemma PartialRightAdjoint.repr_homEquiv_symm_comp {G : F.PartialRightAdjointSource ⥤ C}
+    (P : PartialRightAdjoint F G) {X Y Z} (f : X ⟶ Y) (a : F.obj Z ⟶ X.obj) :
+    (P.repr Y).homEquiv.symm (a ≫ f) = (P.repr X).homEquiv.symm a ≫ G.map f := by
+  rw [Equiv.symm_apply_eq, repr_homEquiv_comp, Equiv.apply_symm_apply]
+
+def PartialRightAdjoint.uniqueUpToIso {G G' : F.PartialRightAdjointSource ⥤ C}
+    (P : PartialRightAdjoint F G) (P' : PartialRightAdjoint F G') : G ≅ G' :=
+  NatIso.ofComponents (fun X => (P.repr _).uniqueUpToIso (P'.repr _))
+  (fun {X Y} f => by
+    apply yoneda.map_injective
+    ext Z a
+    simp only [yoneda_obj_obj, RepresentableBy.uniqueUpToIso_hom, comp_obj, op_obj, map_comp,
+      FullyFaithful.map_preimage, FunctorToTypes.comp, yoneda_map_app, NatIso.ofComponents_hom_app,
+      Function.comp_apply]
+    calc (P'.repr Y).homEquiv.symm ((P.repr Y).homEquiv (a ≫ G.map f))
+    _ = (P'.repr Y).homEquiv.symm ((P.repr X).homEquiv a ≫ f) := by
+      simpa using PartialRightAdjoint.repr_homEquiv_comp ..
+    _ = (P'.repr X).homEquiv.symm ((P.repr X).homEquiv a) ≫ G'.map f := by
+      apply repr_homEquiv_symm_comp)
+
+noncomputable abbrev isoPartialRightAdjoint (G : F.PartialRightAdjointSource ⥤ C)
+    (P : PartialRightAdjoint F G) : G ≅ partialRightAdjoint F :=
+    PartialRightAdjoint.uniqueUpToIso _ P (PartialRightAdjoint.partialRightAdjoint _)

HoTTLean/ForMathlib/CategoryTheory/Bicategory/Grothendieck.lean

@@ -56,12 +56,24 @@ section
 variable {B : Type u₁} [Bicategory B]
 variable (F : Pseudofunctor B Cat) {a b : B}
 
+
 @[simp] lemma _root_.CategoryTheory.LocallyDiscrete.Iso.hom_inv {C : Type u₁} [Category C]
     (X Y : LocallyDiscrete C) (e : X ≅ Y) : e.hom.toLoc ≫ e.inv.toLoc = 𝟙 _ :=
   LocallyDiscrete.eq_of_hom ⟨⟨by simp⟩⟩
 
-attribute [reassoc] StrongTrans.naturality_comp_inv_app
-
+-- Autogenerated by adding @[to_app (attr := reassoc)] to `StrongTrans.naturality_comp_inv`
+def StrongTrans.naturality_comp_inv_app_assoc
+    {B : Type*} [Bicategory B]
+    {F G : Pseudofunctor B Cat} (α : F ⟶ G) {a b c : B} (f : a ⟶ b) (g : b ⟶ c)
+    (X : ↑(F.obj a)) {Z : ↑(G.obj c)} (h : (F.map (f ≫ g) ≫ α.app c).obj X ⟶ Z) :
+    (α.naturality (f ≫ g)).inv.app X ≫ h =
+    (G.mapComp f g).hom.app ((α.app a).obj X) ≫
+    (α_ (α.app a) (G.map f) (G.map g)).inv.app X ≫
+    (G.map g).map ((α.naturality f).inv.app X) ≫
+    (α_ (F.map f) (α.app b) (G.map g)).hom.app X ≫
+    (α.naturality g).inv.app ((F.map f).obj X) ≫
+    (α_ (F.map f) (F.map g) (α.app c)).inv.app X ≫ (α.app c).map ((F.mapComp f g).inv.app X) ≫ h :=
+  sorry
 end
 
 lemma _root_.CategoryTheory.Functor.toPseudofunctor'_map₂ {C : Type u₁} [Category.{v₁} C] (F : C ⥤ Cat)
@@ -1179,7 +1191,7 @@ include hom_id in
 lemma functorFromCompHom_id (c : C) : functorFromCompHom fib hom G (𝟙 c)
     = eqToHom (by simp [Cat.id_eq_id, Functor.id_comp]) := by
   ext x
-  simp [hom_id, functorFromCompHom]
+  simp [hom_id, eqToHom_map, functorFromCompHom]
 
 include hom_comp in
 lemma functorFromCompHom_comp (c₁ c₂ c₃ : C) (f : c₁ ⟶ c₂) (g : c₂ ⟶ c₃):
@@ -1188,7 +1200,7 @@ lemma functorFromCompHom_comp (c₁ c₂ c₃ : C) (f : c₁ ⟶ c₂) (g : c₂
     Functor.whiskerLeft (F.map f) (functorFromCompHom fib hom G g) ≫
     eqToHom (by simp[Cat.comp_eq_comp, Functor.map_comp, Functor.assoc]) := by
   ext
-  simp [functorFromCompHom, hom_comp]
+  simp [functorFromCompHom, hom_comp, eqToHom_map]
 
 theorem functorFrom_comp : functorFrom fib hom hom_id hom_comp ⋙ G =
     functorFrom (functorFromCompFib fib G) (functorFromCompHom fib hom G)