one sorry away from a correct definition

InfinityCosmos.lean

@@ -5,6 +5,7 @@ import InfinityCosmos.ForMathlib.AlgebraicTopology.SimplicialSet.CoherentIso
 import InfinityCosmos.ForMathlib.AlgebraicTopology.SimplicialSet.Homotopy
 import InfinityCosmos.ForMathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
 import InfinityCosmos.ForMathlib.AlgebraicTopology.SimplicialSet.MorphismProperty
+import InfinityCosmos.ForMathlib.AlgebraicTopology.SimplicialSet.Quasicategory
 import InfinityCosmos.ForMathlib.AlgebraicTopology.SimplicialSet.Wombat
 import InfinityCosmos.ForMathlib.CategoryTheory.Enriched.Cotensors
 import InfinityCosmos.ForMathlib.CategoryTheory.Enriched.MonoidalProdCat

InfinityCosmos/ForMathlib/AlgebraicTopology/SimplicialCategory/Limits.lean

@@ -167,6 +167,17 @@ variable {J C}
 
 end ConicalLimits
 
+
+section ConicalTerminal
+variable (C : Type u) [Category.{v} C] [SimplicialCategory C]
+
+/-- An abbreviation for `HasSLimit (Discrete.functor f)`. -/
+abbrev HasConicalTerminal := HasConicalLimitsOfShape (Discrete.{0} PEmpty)
+
+instance HasConicalTerminal_hasTerminal [hyp : HasConicalTerminal C] : HasTerminal C := by
+  infer_instance
+
+end ConicalTerminal
 section ConicalProducts
 variable {C : Type u} [Category.{v} C] [SimplicialCategory C]
 
@@ -195,15 +206,22 @@ instance HasConicalProducts_hasProducts [hyp : HasConicalProducts.{w, v, u} C] :
 
 end ConicalProducts
 
-section ConicalTerminalObject
-variable (C : Type u) [Category.{v} C] [SimplicialCategory C]
+section ConicalPullbacks
+variable {C : Type u} [Category.{v} C] [SimplicialCategory C]
 
-/-- An abbreviation for `HasSLimit (Discrete.functor f)`. -/
-abbrev HasConicalTerminal := HasConicalLimitsOfShape (Discrete.{0} PEmpty)
+abbrev HasConicalPullback {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) := HasConicalLimit (cospan f g)
 
-instance HasConicalTerminal_hasTerminal [hyp : HasConicalTerminal C] : HasTerminal C := by
+instance HasConicalPullback_hasPullback {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z)
+    [HasConicalPullback f g] : HasPullback f g := HasConicalLimit_hasLimit (cospan f g)
+
+variable (C) in
+abbrev HasConicalPullbacks : Prop := HasConicalLimitsOfShape WalkingCospan C
+
+instance HasConicalPullbacks_hasPullbacks [HasConicalPullbacks C] : HasPullbacks C := by
   infer_instance
 
-end ConicalTerminalObject
+end ConicalPullbacks
+
+-- TODO: Add something for conical inverse limits of towers?
 
 end CategoryTheory

InfinityCosmos/ForMathlib/InfinityCosmos/Basic.lean

@@ -28,12 +28,12 @@ open PreInfinityCosmos
 
 /-- Common notation for the hom-spaces in a pre-∞-cosmos.-/
 abbrev Fun (X Y : K) : QCat where
-  obj := EnrichedCategory.Hom (V := SSet) X Y
+  obj := EnrichedCategory.Hom X Y
   property := by
     have : PreInfinityCosmos K := by infer_instance
     have := this.has_qcat_homs (X := X) (Y := Y)
-    convert this
     -- exact this
+    convert this
     sorry
 
 noncomputable def representableMap' {X A B : K} (f : 𝟙_ SSet ⟶ EnrichedCategory.Hom A B) :
@@ -44,14 +44,18 @@ noncomputable def representableMap (X : K) {A B : K} (f : A ⟶ B) :
     (EnrichedCategory.Hom X A : SSet) ⟶ (EnrichedCategory.Hom X B) :=
   representableMap' ((homEquiv A B) f)
 
-noncomputable def representableQCatMap (X : K) {A B : K} (f : A ⟶ B) :
+noncomputable def toFunMap (X : K) {A B : K} (f : A ⟶ B) :
     Fun X A ⟶ Fun X B := representableMap X f
 
 def IsoFibration (X Y : K) : Type v := {f : X ⟶ Y // IsIsoFibration f}
 
 infixr:25  " ↠ " => IsoFibration
 
-variable (K) in
+end InfinityCosmos
+
+open InfinityCosmos
+variable (K : Type u) [Category.{v} K][SimplicialCategory K] [PreInfinityCosmos.{v} K]
+
 /-- Experimenting with some changes.-/
 class InfinityCosmos' extends PreInfinityCosmos K where
   comp_isIsoFibration {X Y Z : K} (f : X ↠ Y) (g : Y ↠ Z) : IsIsoFibration (f.1 ≫ g.1)
@@ -62,12 +66,12 @@ class InfinityCosmos' extends PreInfinityCosmos K where
   prod_map_fibrant {γ : Type w} {A B : γ → K} (f : ∀ i, A i ⟶ B i) :
     (∀ i, IsIsoFibration (f i)) → IsIsoFibration (Limits.Pi.map f)
   [has_isoFibration_pullbacks {X Y Z : K} (f : X ⟶ Y) (g : Z ⟶ Y) :
-    IsIsoFibration g → HasPullback f g] -- TODO: make simplicially enriched
+    IsIsoFibration g → HasConicalPullback f g]
   pullback_is_isoFibration {X Y Z P : K} (f : X ⟶ Z) (g : Y ⟶ Z)
     (fst : P ⟶ X) (snd : P ⟶ Y) (h : IsPullback fst snd f g) :
     IsIsoFibration g → IsIsoFibration fst
   [has_limits_of_towers (F : ℕᵒᵖ ⥤ K) :
-    (∀ n : ℕ, IsIsoFibration (F.map (homOfLE (Nat.le_succ n)).op)) → HasLimit F] -- TODO: make conical
+    (∀ n : ℕ, IsIsoFibration (F.map (homOfLE (Nat.le_succ n)).op)) → HasConicalLimit F]
   has_limits_of_towers_isIsoFibration (F : ℕᵒᵖ ⥤ K) (hf) :
     haveI := has_limits_of_towers F hf
     IsIsoFibration (limit.π F (.op 0))
@@ -77,29 +81,25 @@ class InfinityCosmos' extends PreInfinityCosmos K where
     (h : IsPullback fst snd (cotensorContraMap i Y) (cotensorCovMap A f)) :
     IsIsoFibration (h.isLimit.lift <|
       PullbackCone.mk (cotensorCovMap B f) (cotensorContraMap i X) (cotensor_bifunctoriality i f))
-  local_isoFibration {X A B : K} (f : A ⟶ B) (hf : IsIsoFibration f) :
-  SSet.IsoFibration (representableQCatMap X f)
+  local_isoFibration {X A B : K} (f : A ⟶ B) (hf : IsIsoFibration f) : IsoFibration (toFunMap X f)
 
 open InfinityCosmos'
 
--- def compIsofibration {hyp : InfinityCosmos' K} {A B C : K} (f : A ↠ B) (g : B ↠ C) : A ↠ C := by
---   fconstructor
---   · exact (f.1 ≫ g.1)
---   · have := hyp.comp_isIsoFibration f g
-
 section tests
 variable {K : Type u} [Category.{v} K][SimplicialCategory K] [PreInfinityCosmos.{v} K]
 [InfinityCosmos' K]
 
--- fails to synthesize HasBinaryProducts
+-- -- fails to synthesize HasBinaryProducts
 -- theorem prod_map_fibrant {X Y X' Y' : K} {f : X ⟶ Y} {g : X' ⟶ Y'} :
 --     IsIsoFibration f → IsIsoFibration g → IsIsoFibration (prod.map f g)
 
-
+-- -- confused about an instance "toPreInfinityCosmos" in the type of g
+-- def compIsofibration {hyp : InfinityCosmos' K} {A B C : K} (f : A ↠ B) (g : B ↠ C) : A ↠ C := by
+--   fconstructor
+--   · exact (f.1 ≫ g.1)
+--   · have := hyp.comp_isIsoFibration f g
 end tests
 
-end InfinityCosmos
-
 class InfinityCosmos extends SimplicialCategory K where
   [has_qcat_homs : ∀ {X Y : K}, SSet.Quasicategory (EnrichedCategory.Hom X Y)]
   IsIsoFibration {X Y : K} : (X ⟶ Y) → Prop
@@ -108,39 +108,25 @@ class InfinityCosmos extends SimplicialCategory K where
   iso_isIsoFibration {X Y : K} (e : X ≅ Y) : IsIsoFibration e.hom
   has_terminal : HasTerminal K
   all_objects_fibrant {X Y : K} (hY : IsTerminal Y) (f : X ⟶ Y) : IsIsoFibration f
-  has_products : HasBinaryProducts K -- TODO: replace by HasConicalProducts
-  prod_map_fibrant {X Y X' Y' : K} {f : X ⟶ Y} {g : X' ⟶ Y'} :
-    IsIsoFibration f → IsIsoFibration g → IsIsoFibration (prod.map f g)
+  has_products : HasConicalProducts K
+  prod_map_fibrant {γ : Type w} {A B : γ → K} (f : ∀ i, A i ⟶ B i) :
+    (∀ i, IsIsoFibration (f i)) → IsIsoFibration (Limits.Pi.map f)
   [has_isoFibration_pullbacks {X Y Z : K} (f : X ⟶ Y) (g : Z ⟶ Y) :
-    IsIsoFibration g → HasPullback f g]
+    IsIsoFibration g → HasConicalPullback f g]
   pullback_is_isoFibration {X Y Z P : K} (f : X ⟶ Z) (g : Y ⟶ Z)
     (fst : P ⟶ X) (snd : P ⟶ Y) (h : IsPullback fst snd f g) :
     IsIsoFibration g → IsIsoFibration fst
   has_limits_of_towers (F : ℕᵒᵖ ⥤ K) :
-    (∀ n : ℕ, IsIsoFibration (F.map (homOfLE (Nat.le_succ n)).op)) → HasLimit F
+    (∀ n : ℕ, IsIsoFibration (F.map (homOfLE (Nat.le_succ n)).op)) → HasConicalLimit F
   has_limits_of_towers_isIsoFibration (F : ℕᵒᵖ ⥤ K) (hf) :
     haveI := has_limits_of_towers F hf
     IsIsoFibration (limit.π F (.op 0))
-  [has_cotensors : HasCotensors K] -- ER: Added
-  -- leibniz_cotensor {X Y : K} (f : X ⟶ Y) (A B : SSet) (i : A ⟶ B) [Mono i]
-  --   (hf : IsIsoFibration f) {P : K} (fst : P ⟶ B ⋔⋔ Y) (snd : P ⟶ A ⋔⋔ X)
-  --   (h : IsPullback fst snd ((cotensor.map (.op i)).app Y) ((cotensor.obj (.op A)).map f)) :
-  --   IsIsoFibration (h.isLimit.lift <|
-  --     PullbackCone.mk ((cotensor.obj (.op B)).map f) ((cotensor.map (.op i)).app X) (by aesop_cat))
+  [has_cotensors : HasCotensors K]
   leibniz_cotensor {X Y : K} (f : X ⟶ Y) (A B : SSet) (i : A ⟶ B) [Mono i]
     (hf : IsIsoFibration f) {P : K} (fst : P ⟶ B ⋔ Y) (snd : P ⟶ A ⋔ X)
     (h : IsPullback fst snd (cotensorContraMap i Y) (cotensorCovMap A f)) :
     IsIsoFibration (h.isLimit.lift <|
       PullbackCone.mk (cotensorCovMap B f) (cotensorContraMap i X) (cotensor_bifunctoriality i f))
-  local_isoFibration {X A B : K} (f : A ⟶ B) (hf : IsIsoFibration f) :
-  IsQCatIsoFibration (representableMap X f)
--- namespace InfinityCosmos
--- variable [InfinityCosmos.{v} K]
-
--- def IsoFibration (X Y : K) : Type v := {f : X ⟶ Y // IsIsoFibration f}
-
--- infixr:25  " ↠ " => IsoFibration
-
--- end InfinityCosmos
+  local_isoFibration {X A B : K} (f : A ⟶ B) (hf : IsIsoFibration f) : IsoFibration (toFunMap X f)
 
 end CategoryTheory