experiment with a notion of homotopy, equivalence, etc, dependent on …

…an interval to specialize to several cases

InfinityCosmos.lean

@@ -1,4 +1,5 @@
 import InfinityCosmos.ForMathlib.AlgebraicTopology.CoherentIso
+import InfinityCosmos.ForMathlib.AlgebraicTopology.Homotopy
 import InfinityCosmos.ForMathlib.AlgebraicTopology.HomotopyCat
 import InfinityCosmos.ForMathlib.AlgebraicTopology.Wombat
 import InfinityCosmos.ForMathlib.CategoryTheory.CodiscreteCat

InfinityCosmos/ForMathlib/AlgebraicTopology/CoherentIso.lean

@@ -88,36 +88,4 @@ open Simplicial SimplicialCategory
 def coherentIso.pt (i : WalkingIso) : Δ[0] ⟶ coherentIso :=
   (yonedaEquiv coherentIso [0]).symm (WalkingIso.coev i)
 
-open MonoidalCategory in
-def pointIsUnit : Δ[0] ≅ (𝟙_ SSet) := by sorry
-
-open MonoidalCategory in
-noncomputable def expUnitNatIso : ihom (𝟙_ SSet) ≅ 𝟭 SSet :=
-  (conjugateIsoEquiv (Adjunction.id (C := SSet)) (ihom.adjunction _)
-    (leftUnitorNatIso _)).symm
-
-def expPointNatIso : ihom Δ[0] ≅ 𝟭 SSet := by sorry
---   refine ?_ ≪≫ expUnitNatIso
---   have := pointIsUnit.symm.op
---   sorry
-
-def expPointIsoSelf (X : SSet) : sHom Δ[0] X ≅ X := sorry -- expPointNatIso.app X
-
-noncomputable def coherentIso.ev (X : SSet) (i : WalkingIso) : sHom coherentIso X ⟶ X :=
-  (MonoidalClosed.pre (coherentIso.pt i)).app X ≫ (expPointIsoSelf X).hom
-
-/-- This is in the wrong file.
-We should add a hypothesis that `A` and `B` are quasi-categories and perhaps move into a
-quasi-category namespace?-/
-structure SHomotopy {A B : SSet.{u}} (f g : A ⟶ B) : Type u where
-  homotopy : A ⟶ sHom coherentIso B
-  source_eq : homotopy ≫ coherentIso.ev B WalkingIso.zero = f
-  target_eq : homotopy ≫ coherentIso.ev B WalkingIso.one = g
-
-structure Equiv (A B : SSet.{u}) : Type u where
-  toFun : A ⟶ B
-  invFun : B ⟶ A
-  left_inv : SHomotopy (toFun ≫ invFun) (𝟙 A)
-  right_inv : SHomotopy (invFun ≫ toFun) (𝟙 B)
-
 end SSet

InfinityCosmos/ForMathlib/AlgebraicTopology/Homotopy.lean

@@ -0,0 +1,78 @@
+/-
+Copyright (c) 2024 Johns Hopkins Category Theory Seminar. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Johns Hopkins Category Theory Seminar
+-/
+
+import InfinityCosmos.ForMathlib.AlgebraicTopology.CoherentIso
+
+universe u v w
+
+namespace SSet
+
+open CategoryTheory Simplicial SimplicialCategory
+
+/-- An interval is a simplicial set equipped with two endpoints.-/
+class Interval (I : SSet.{u}) : Type u where
+  src : Δ[0] ⟶ I
+  tgt : Δ[0] ⟶ I
+
+/-- The interval relevant to the theory of Kan complexes.-/
+instance arrowInterval : Interval Δ[1] where
+  src := standardSimplex.map (SimplexCategory.δ (n := 0) (1))
+  tgt := standardSimplex.map (SimplexCategory.δ (n := 0) (0))
+
+/-- The interval relevant to the theory of quasi-categories. -/
+instance isoInterval : Interval coherentIso where
+  src :=   (yonedaEquiv coherentIso [0]).symm (WalkingIso.coev WalkingIso.zero)
+  tgt :=   (yonedaEquiv coherentIso [0]).symm (WalkingIso.coev WalkingIso.one)
+
+
+open MonoidalCategory
+def pointIsUnit : Δ[0] ≅ (𝟙_ SSet) := by sorry
+
+noncomputable def expUnitNatIso : ihom (𝟙_ SSet) ≅ 𝟭 SSet :=
+  (conjugateIsoEquiv (Adjunction.id (C := SSet)) (ihom.adjunction _)
+    (leftUnitorNatIso _)).symm
+
+def expPointNatIso : ihom Δ[0] ≅ 𝟭 SSet := by sorry
+--   refine ?_ ≪≫ expUnitNatIso
+--   have := pointIsUnit.symm.op
+--   sorry
+
+/-- Once we've proven that `Δ[0]` is terminal, this will follow from something just PRed to mathlib.-/
+def expPointIsoSelf (X : SSet) : sHom Δ[0] X ≅ X := sorry
+
+section
+
+variable {I : SSet.{u}} [Interval I]
+
+noncomputable def pathSpace {I : SSet.{u}} [Interval I] (X : SSet.{u}) : SSet.{u} := sHom I X
+
+open MonoidalClosed
+
+noncomputable def pathSpace.src (X : SSet.{u}) : pathSpace (I := I) X ⟶ X :=
+  ((MonoidalClosed.pre Interval.src).app X ≫ X.expPointIsoSelf.hom)
+
+noncomputable def pathSpace.tgt (X : SSet.{u}) : pathSpace (I := I) X ⟶ X :=
+  ((MonoidalClosed.pre Interval.tgt).app X ≫ X.expPointIsoSelf.hom)
+
+
+/-- TODO: Figure out how to allow `I` to be an a different universe from `A` and `B`?-/
+structure Homotopy {A B : SSet.{u}} (f g : A ⟶ B) : Type u
+    where
+  homotopy : A ⟶ sHom I B
+  source_eq : homotopy ≫ pathSpace.src B = f
+  target_eq : homotopy ≫ pathSpace.tgt B = g
+
+/-- For the correct interval, this defines a good notion of equivalences for both Kan complexes
+and quasi-categories.-/
+structure Equiv (A B : SSet.{u}) : Type u where
+  toFun : A ⟶ B
+  invFun : B ⟶ A
+  left_inv : Homotopy (I := I) (toFun ≫ invFun) (𝟙 A)
+  right_inv : Homotopy (I := I) (invFun ≫ toFun) (𝟙 B)
+
+end
+
+end SSet