Add several sorry'd definitions according to FS22

SOAS/CategoryOfFamilies.lean

@@ -0,0 +1,58 @@
+import Mathlib.CategoryTheory.Category.Basic
+import Mathlib.CategoryTheory.Closed.Cartesian
+import Mathlib.CategoryTheory.Limits.Shapes.FiniteProducts
+import SOAS.Paper
+
+open CategoryTheory
+
+
+-- in soas-agda there is a definition of `𝔽amilies` (category of indexed families)
+-- and `𝕊orted`, that turns a category into a sorted category
+-- https://github.com/DimaSamoz/agda-soas/blob/9f4cca21e3e80ae35ec1b796e3f49b8a3e64ccbe/SOAS/Families/Core.agda
+-- https://github.com/DimaSamoz/agda-soas/blob/9f4cca21e3e80ae35ec1b796e3f49b8a3e64ccbe/SOAS/Sorting.agda
+
+instance : CategoryStruct (Familyₛ T) where
+  Hom := s_family_map
+  id := λ _ => id
+  comp := λ {C1 C2 C3} (r1 : s_family_map C1 C2) (r2 : s_family_map C2 C3) => r2 ∘ r1
+
+instance 𝔽amiliesₛ : Category (Familyₛ T) where
+  id_comp := by aesop_cat
+  comp_id := by aesop_cat
+  assoc := by aesop_cat
+
+-- A bicartesian closed category is a cartesian closed category with finite coproducts
+
+def limitCone (F : Discrete (Fin n) ⥤ Familyₛ T) : Limits.LimitCone F where
+  cone := sorry
+  isLimit := sorry
+
+def colimitCone (F : Discrete (Fin n) ⥤ Familyₛ T) : Limits.ColimitCocone F where
+  cocone := sorry
+  isColimit := sorry
+
+instance (F : Discrete (Fin n) ⥤ Familyₛ T) : Limits.HasLimit F where
+  exists_limit := Nonempty.intro (limitCone F)
+
+instance (F : Discrete (Fin n) ⥤ Familyₛ T) : Limits.HasColimit F where
+  exists_colimit := Nonempty.intro (colimitCone F)
+
+instance (n : ℕ) : Limits.HasLimitsOfShape (Discrete (Fin n)) (Familyₛ T) where
+instance (n : ℕ) : Limits.HasColimitsOfShape (Discrete (Fin n)) (Familyₛ T) where
+
+instance : Limits.HasFiniteProducts (Familyₛ T) where
+  out := fun n => by infer_instance
+
+instance : MonoidalCategory (Familyₛ T) := sorry -- where
+  -- tensorObj := sorry
+  -- whiskerLeft := sorry
+  -- whiskerRight := sorry
+  -- tensorUnit := sorry
+  -- associator := sorry
+  -- leftUnitor := sorry
+  -- rightUnitor := sorry
+
+instance : CartesianClosed (Familyₛ T) := sorry
+
+instance : Limits.HasFiniteCoproducts (Familyₛ T) where
+  out := fun n => by infer_instance

SOAS/CategoryOfRenamings.lean

@@ -0,0 +1,40 @@
+import Mathlib.CategoryTheory.Category.Basic
+import Mathlib.CategoryTheory.Limits.Shapes.FiniteProducts
+import SOAS.Paper
+
+open CategoryTheory
+variable (T : Type)
+
+-- https://github.com/DimaSamoz/agda-soas/blob/9f4cca21e3e80ae35ec1b796e3f49b8a3e64ccbe/SOAS/ContextMaps/CategoryOfRenamings.agda#L22
+instance : CategoryStruct (Ctx T) where
+  Hom := Ctx.rename
+  id := λ _ => id
+  comp := λ {C1 C2 C3} (r1 : Ctx.rename C1 C2) (r2 : Ctx.rename C2 C3) => r2 ∘ r1
+
+instance 𝔽 : Category (Ctx T) where
+  id_comp := by aesop_cat
+  comp_id := by aesop_cat
+  assoc := by aesop_cat
+
+def colimitCocone (F : Discrete Limits.WalkingPair ⥤ Ctx T) : Limits.ColimitCocone F
+  := {
+    cocone := {
+      pt := sorry,
+      ι := sorry
+    }
+    isColimit := {
+      desc := sorry
+      fac := sorry
+      uniq := sorry
+    }
+  }
+
+instance hasColimitF
+  (F : Discrete Limits.WalkingPair ⥤ Ctx T): Limits.HasColimit F where
+  exists_colimit := Nonempty.intro (colimitCocone T F)
+
+instance boo : Limits.HasColimitsOfShape (Discrete Limits.WalkingPair) (Ctx T) where
+  has_colimit : ∀ F, Limits.HasColimit F := by infer_instance
+
+-- is it same as cocartesian?
+instance : Limits.HasBinaryCoproducts (Ctx T) where

SOAS/Coalgebra.lean

@@ -0,0 +1,16 @@
+import Mathlib.RingTheory.Coalgebra.Basic
+import SOAS.Paper
+
+instance : CommSemiring (Familyₛ T) := sorry
+instance : AddCommMonoid a := sorry
+instance : Module (Familyₛ T) a := sorry
+
+-- what to put instead of a?
+instance : CoalgebraStruct (Familyₛ T) a where
+  comul := sorry
+  counit := sorry
+
+instance : Coalgebra (Familyₛ T) a where
+  coassoc := sorry
+  rTensor_counit_comp_comul := sorry
+  lTensor_counit_comp_comul := sorry

lakefile.lean

@@ -16,3 +16,4 @@ require batteries from
 lean_lib PhiCalculus
 
 lean_lib Minimal
+lean_lib SOAS