Fill in some admitted proofs

InfinityCosmos/ForMathlib/AlgebraicTopology/SimplicialCategory/IsConicalTerminal.lean

@@ -17,28 +17,27 @@ 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
+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 `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 } }
+/-- Transport a term of type `IsConicalTerminal` across an isomorphism. -/
+noncomputable def IsConicalTerminal.ofIso {Y Z : C} (hY : IsConicalTerminal Y)
+    (i : Y ≅ Z) : IsConicalTerminal Z :=
+  hY.ofIsoSLimit <| Cones.ext 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
+noncomputable def conicalTerminalIsConicalTerminal :
+    IsConicalTerminal (conicalTerminal C) :=
+  conicalLimit.isConicalLimit _ |>.ofIsoSLimit <| Cones.ext (by rfl) (by simp)
 
-def terminalIsConicalTerminal {T : C} (hT : IsTerminal T) :
+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/AlgebraicTopology/SimplicialCategory/Limits.lean

@@ -26,6 +26,19 @@ structure IsSLimit where
 /-- Conical simplicial limits are also limits in the unenriched sense.-/
 def IsSLimit_islimit (slim : IsSLimit c) : IsLimit c := slim.isLimit
 
+/-- Transport evidence that a cone is a simplicially enriched limit cone across
+an isomorphism of cones. -/
+noncomputable def IsSLimit.ofIsoSLimit {r t : Cone F} (h : IsSLimit r)
+    (i : r ≅ t) : IsSLimit t where
+  isLimit := h.isLimit.ofIsoLimit i
+  isSLimit X := h.isSLimit X |>.ofIsoLimit
+    { hom := Functor.mapConeMorphism _ i.hom
+      inv := Functor.mapConeMorphism _ i.inv
+      hom_inv_id := by
+        simp only [Functor.mapCone, Functor.mapConeMorphism, Iso.map_hom_inv_id]
+      inv_hom_id := by
+        simp only [Functor.mapCone, Functor.mapConeMorphism, Iso.map_inv_hom_id] }
+
 namespace SimplicialCategory
 
 /-!

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