Fill in some admitted proofs

InfinityCosmos.lean

@@ -12,6 +12,7 @@ import InfinityCosmos.ForMathlib.AlgebraicTopology.SimplicialSet.Monoidal
 import InfinityCosmos.ForMathlib.AlgebraicTopology.SimplicialSet.MorphismProperty
 import InfinityCosmos.ForMathlib.CategoryTheory.Enriched.Cotensors
 import InfinityCosmos.ForMathlib.CategoryTheory.Enriched.MonoidalProdCat
+import InfinityCosmos.ForMathlib.CategoryTheory.Enriched.Ordinary
 import InfinityCosmos.ForMathlib.CategoryTheory.MorphismProperty
 import InfinityCosmos.ForMathlib.InfinityCosmos.Basic
 import InfinityCosmos.ForMathlib.InfinityCosmos.Isofibrations

InfinityCosmos/ForMathlib/AlgebraicTopology/SimplicialCategory/Basic.lean

@@ -3,6 +3,7 @@ Copyright (c) 2024 Joël Riou. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joël Riou
 -/
+import InfinityCosmos.ForMathlib.CategoryTheory.Enriched.Ordinary
 import Mathlib.AlgebraicTopology.SimplicialCategory.Basic
 import Mathlib.CategoryTheory.Closed.Cartesian
 import Mathlib.CategoryTheory.Closed.FunctorToTypes
@@ -45,6 +46,9 @@ variable {C : Type u} [Category.{v} C] [SimplicialCategory C]
 noncomputable abbrev sHomWhiskerRight {K K' : C} (f : K ⟶ K') (L : C) :
     sHom K' L ⟶ sHom K L := eHomWhiskerRight SSet f L
 
+noncomputable abbrev sHomWhiskerRightIso {K K' : C} (i : K ≅ K') (L : C) :
+    sHom K' L ≅ sHom K L := eHomWhiskerRightIso SSet i L
+
 @[simp]
 lemma sHomWhiskerRight_id (K L : C) : sHomWhiskerRight (𝟙 K) L = 𝟙 _ :=
   eHomWhiskerRight_id _ K L
@@ -58,6 +62,9 @@ lemma sHomWhiskerRight_comp {K K' K'' : C} (f : K ⟶ K') (f' : K' ⟶ K'') (L :
 noncomputable abbrev sHomWhiskerLeft (K : C) {L L' : C} (g : L ⟶ L') :
     sHom K L ⟶ sHom K L' := eHomWhiskerLeft SSet K g
 
+noncomputable abbrev sHomWhiskerLeftIso (K : C) {L L' : C} (i : L ≅ L') :
+    sHom K L ≅ sHom K L' := eHomWhiskerLeftIso SSet K i
+
 @[simp]
 lemma sHomWhiskerLeft_id (K L : C) : sHomWhiskerLeft K (𝟙 L) = 𝟙 _ :=
   eHomWhiskerLeft_id _ _ _

InfinityCosmos/ForMathlib/AlgebraicTopology/SimplicialCategory/IsConicalTerminal.lean

@@ -17,28 +17,37 @@ abbrev IsConicalTerminal (T : C) := IsSLimit (asEmptyCone T)
 def IsConicalTerminal.isTerminal {T : C} (hT : IsConicalTerminal T) : IsTerminal T := hT.isLimit
 
 /-- The defining universal property of a conical terminal object gives an isomorphism of homs.-/
-def IsConicalTerminal.sHomIso {T : C} (hT : IsConicalTerminal T) (X : C) : sHom X T ≅ ⊤_ SSet := by
-  let iso : sHom X T ≅ _ := limitComparisonIso _ X hT
-  sorry
-
-/-- Transport a term of type `IsTerminal` across an isomorphism. -/
-def IsConicalTerminal.ofIso {Y Z : C} (hY : IsConicalTerminal Y) (i : Y ≅ Z) :
-    IsConicalTerminal Z := sorry
-  -- IsLimit.ofIsoLimit hY
-  --   { hom := { hom := i.hom }
-  --     inv := { hom := i.inv } }
+noncomputable def IsConicalTerminal.sHomIso {T : C} (hT : IsConicalTerminal T)
+    (X : C) : sHom X T ≅ ⊤_ SSet :=
+  limitComparisonIso _ X hT ≪≫
+    HasLimit.isoOfEquivalence (by rfl) (Functor.emptyExt _ _)
+
+/-- Transport a term of type `IsConicalTerminal` across an isomorphism. -/
+noncomputable def IsConicalTerminal.ofIso {Y Z : C} (hY : IsConicalTerminal Y) (i : Y ≅ Z) :
+    IsConicalTerminal Z where
+  isLimit := IsTerminal.ofIso hY.isTerminal i
+  isSLimit X :=
+    hY.isSLimit X |>.ofIsoLimit <| Cones.ext (sHomWhiskerLeftIso X i) (by simp)
 
 namespace HasConicalTerminal
 variable [HasConicalTerminal C]
 
 variable (C) in
 noncomputable def conicalTerminal : C := conicalLimit (Functor.empty.{0} C)
 
-def conicalTerminalIsConicalTerminal : IsConicalTerminal (conicalTerminal C) where
-  isLimit := sorry
-  isSLimit := sorry
-
-def terminalIsConicalTerminal {T : C} (hT : IsTerminal T) :
+noncomputable def conicalTerminalIsConicalTerminal :
+    IsConicalTerminal (conicalTerminal C) where
+  isLimit := by
+    let h := conicalLimit.isConicalLimit (Functor.empty.{0} C)
+    exact h.isLimit.ofIsoLimit <| Cones.ext (by rfl) (by simp)
+  isSLimit X := by
+    let h := conicalLimit.isConicalLimit (Functor.empty.{0} C)
+    apply h.isSLimit X |>.ofIsoLimit
+    refine Cones.ext ?_ (by simp)
+    dsimp only [Functor.mapCone_pt]
+    rfl
+
+noncomputable def terminalIsConicalTerminal {T : C} (hT : IsTerminal T) :
     IsConicalTerminal T := by
   let TT := conicalLimit (Functor.empty.{0} C)
   let slim : IsConicalTerminal TT := conicalTerminalIsConicalTerminal

InfinityCosmos/ForMathlib/CategoryTheory/Enriched/Ordinary.lean

@@ -0,0 +1,30 @@
+import Mathlib.CategoryTheory.Enriched.Ordinary
+
+universe v' v u u'
+
+open CategoryTheory Category MonoidalCategory
+
+namespace CategoryTheory
+
+variable (V : Type u') [Category.{v'} V] [MonoidalCategory V]
+  {C : Type u} [Category.{v} C] [EnrichedOrdinaryCategory V C]
+
+def eHomWhiskerLeftIso (X : C) {Y Y' : C} (i : Y ≅ Y') :
+    (X ⟶[V] Y) ≅ (X ⟶[V] Y') where
+  hom := eHomWhiskerLeft V X i.hom
+  inv := eHomWhiskerLeft V X i.inv
+  hom_inv_id := by
+    rw [← eHomWhiskerLeft_comp, i.hom_inv_id, eHomWhiskerLeft_id]
+  inv_hom_id := by
+    rw [← eHomWhiskerLeft_comp, i.inv_hom_id, eHomWhiskerLeft_id]
+
+def eHomWhiskerRightIso {X X' : C} (i : X ≅ X') (Y : C) :
+    (X' ⟶[V] Y) ≅ (X ⟶[V] Y) where
+  hom := eHomWhiskerRight V i.hom Y
+  inv := eHomWhiskerRight V i.inv Y
+  hom_inv_id := by
+    rw [← eHomWhiskerRight_comp, i.inv_hom_id, eHomWhiskerRight_id]
+  inv_hom_id := by
+    rw [← eHomWhiskerRight_comp, i.hom_inv_id, eHomWhiskerRight_id]
+
+end CategoryTheory

InfinityCosmos/ForMathlib/InfinityCosmos/Basic.lean

@@ -89,7 +89,7 @@ instance : HasConicalTerminal K := by infer_instance
 instance : HasTerminal K := by infer_instance
 
 /-- The terminal object in an ∞-cosmos is a conical terminal object. -/
-def terminalIsConicalTerminal : IsConicalTerminal (⊤_ K) :=
+noncomputable def terminalIsConicalTerminal : IsConicalTerminal (⊤_ K) :=
   HasConicalTerminal.terminalIsConicalTerminal terminalIsTerminal
 
 instance : HasCotensors K := by infer_instance