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

An interval is a simplicial set equipped with two endpoints.

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

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

The interval relevant to the theory of Kan complexes.

Equations

• SSet.arrowInterval = { src := SSet.stdSimplex.δ 1, tgt := SSet.stdSimplex.δ 0 }

instance SSet.isoInterval : coherentIso.Interval

The interval relevant to the theory of quasi-categories.

Equations

• SSet.isoInterval = { src := SSet.yonedaEquiv.symm CategoryTheory.WalkingIso.zero.coev, tgt := SSet.yonedaEquiv.symm CategoryTheory.WalkingIso.one.coev }

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

Equations

• SSet.pointIsUnit = SSet.isTerminalDeltaZero.uniqueUpToIso (CategoryTheory.Limits.IsTerminal.ofUnique (𝟙_ SSet))

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

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

Equations

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

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

Equations

• X.expPointIsoSelf = SSet.expPointNatIso.app X

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) : 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) : 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 (pathSpace.src B) = f
• target_eq : CategoryTheory.CategoryStruct.comp self.homotopy (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 : Homotopy (CategoryTheory.CategoryStruct.comp self.toFun self.invFun) (CategoryTheory.CategoryStruct.id A)
• right_inv : Homotopy (CategoryTheory.CategoryStruct.comp self.invFun self.toFun) (CategoryTheory.CategoryStruct.id B)

structure SSet.HomotopyL {A : SSet} (f g : A.obj (Opposite.op (SimplexCategory.mk 1))) : Type u

• simplex : A.obj (Opposite.op (SimplexCategory.mk 2))
• δ₀_eq : CategoryTheory.SimplicialObject.δ A 0 self.simplex = CategoryTheory.SimplicialObject.σ A 0 (CategoryTheory.SimplicialObject.δ A 0 f)
• δ₁_eq : CategoryTheory.SimplicialObject.δ A 1 self.simplex = g
• δ₂_eq : CategoryTheory.SimplicialObject.δ A 2 self.simplex = f

structure SSet.HomotopyR {A : SSet} (f g : A.obj (Opposite.op (SimplexCategory.mk 1))) : Type u

• simplex : A.obj (Opposite.op (SimplexCategory.mk 2))
• δ₀_eq : CategoryTheory.SimplicialObject.δ A 0 self.simplex = f
• δ₁_eq : CategoryTheory.SimplicialObject.δ A 1 self.simplex = g
• δ₂_eq : CategoryTheory.SimplicialObject.δ A 2 self.simplex = CategoryTheory.SimplicialObject.σ A 0 (CategoryTheory.SimplicialObject.δ A 1 f)

def SSet.HomotopicL {A : SSet} (f g : A.obj (Opposite.op (SimplexCategory.mk 1))) : Prop

Equations

• SSet.HomotopicL f g = Nonempty (SSet.HomotopyL f g)

def SSet.HomotopicR {A : SSet} (f g : A.obj (Opposite.op (SimplexCategory.mk 1))) : Prop

Equations

• SSet.HomotopicR f g = Nonempty (SSet.HomotopyR f g)

def SSet.HomotopyL.refl {A : SSet} (f : A.obj (Opposite.op (SimplexCategory.mk 1))) : HomotopyL f f

Equations

• SSet.HomotopyL.refl f = { simplex := CategoryTheory.SimplicialObject.σ A 1 f, δ₀_eq := ⋯, δ₁_eq := ⋯, δ₂_eq := ⋯ }

noncomputable def SSet.HomotopyL.ofHomotopyLOfHomotopyL {A : SSet} {f g h : A.obj (Opposite.op (SimplexCategory.mk 1))} (H₁ : HomotopyL f g) (H₂ : HomotopyL f h) : HomotopyL g h

Equations

• H₁.ofHomotopyLOfHomotopyL H₂ = { simplex := CategoryTheory.SimplicialObject.δ A 1 sorry, δ₀_eq := ⋯, δ₁_eq := ⋯, δ₂_eq := ⋯ }

theorem SSet.HomotopyL.equiv {A : SSet} : Equivalence fun (f g : A.obj (Opposite.op (SimplexCategory.mk 1))) => HomotopicL f g

theorem SSet.homotopicL_iff_homotopicR {A : SSet} (f g : A.obj (Opposite.op (SimplexCategory.mk 1))) [A.Quasicategory] : HomotopicL f g ↔ HomotopicR f g

theorem SSet.HomotopyR.equiv {A : SSet} [A.Quasicategory] : Equivalence fun (f g : A.obj (Opposite.op (SimplexCategory.mk 1))) => HomotopicR f g