class SSet.Interval (I : SSet) : Type u

An interval is a simplicial set equipped with two endpoints.

• src : SSet.standardSimplex.obj (SimplexCategory.mk 0) ⟶ I
• tgt : SSet.standardSimplex.obj (SimplexCategory.mk 0) ⟶ I

instance SSet.arrowInterval : (SSet.standardSimplex.obj (SimplexCategory.mk 1)).Interval

The interval relevant to the theory of Kan complexes.

Equations

• SSet.arrowInterval = { src := SSet.standardSimplex.map (SimplexCategory.δ 1), tgt := SSet.standardSimplex.map (SimplexCategory.δ 0) }

instance SSet.isoInterval : SSet.coherentIso.Interval

The interval relevant to the theory of quasi-categories.

Equations

• One or more equations did not get rendered due to their size.

def SSet.pointIsUnit : SSet.standardSimplex.obj (SimplexCategory.mk 0) ≅ 𝟙_ SSet

Equations

• SSet.pointIsUnit = sorry

noncomputable def SSet.expUnitNatIso : CategoryTheory.ihom (𝟙_ SSet) ≅ CategoryTheory.Functor.id SSet

Equations

• SSet.expUnitNatIso = ((CategoryTheory.conjugateIsoEquiv CategoryTheory.Adjunction.id (CategoryTheory.ihom.adjunction (𝟙_ SSet))) (CategoryTheory.MonoidalCategory.leftUnitorNatIso SSet)).symm

def SSet.expPointNatIso : CategoryTheory.ihom (SSet.standardSimplex.obj (SimplexCategory.mk 0)) ≅ CategoryTheory.Functor.id SSet

Equations

• SSet.expPointNatIso = sorry

def SSet.expPointIsoSelf (X : SSet) : CategoryTheory.SimplicialCategory.sHom (SSet.standardSimplex.obj (SimplexCategory.mk 0)) X ≅ X

Once we've proven that Δ[0] is terminal, this will follow from something just PRed to mathlib.

Equations

• X.expPointIsoSelf = sorry

noncomputable def SSet.pathSpace {I : SSet} [I.Interval] (X : SSet) : SSet

Equations

• SSet.pathSpace X = CategoryTheory.SimplicialCategory.sHom I X

noncomputable def SSet.pathSpace.src {I : SSet} [I.Interval] (X : SSet) : SSet.pathSpace X ⟶ X

Equations

• SSet.pathSpace.src X = CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalClosed.pre SSet.Interval.src).app X) X.expPointIsoSelf.hom

noncomputable def SSet.pathSpace.tgt {I : SSet} [I.Interval] (X : SSet) : SSet.pathSpace X ⟶ X

Equations

• SSet.pathSpace.tgt X = CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalClosed.pre SSet.Interval.tgt).app X) X.expPointIsoSelf.hom

structure SSet.Homotopy {I : SSet} [I.Interval] {A B : SSet} (f g : A ⟶ B) : Type u

TODO: Figure out how to allow I to be an a different universe from A and B?

• homotopy : A ⟶ CategoryTheory.SimplicialCategory.sHom I B
• source_eq : CategoryTheory.CategoryStruct.comp self.homotopy (SSet.pathSpace.src B) = f
• target_eq : CategoryTheory.CategoryStruct.comp self.homotopy (SSet.pathSpace.tgt B) = g

structure SSet.Equiv {I : SSet} [I.Interval] (A B : SSet) : Type u

For the correct interval, this defines a good notion of equivalences for both Kan complexes and quasi-categories.

• toFun : A ⟶ B
• invFun : B ⟶ A
• left_inv : SSet.Homotopy (CategoryTheory.CategoryStruct.comp self.toFun self.invFun) (CategoryTheory.CategoryStruct.id A)
• right_inv : SSet.Homotopy (CategoryTheory.CategoryStruct.comp self.invFun self.toFun) (CategoryTheory.CategoryStruct.id B)