inductive SSet.BoundaryInclusion {X Y : SSet} : (X ⟶ Y) → Prop

an inductive type defining boundary inclusions as a class of morphisms. Used to take advantage of the MorphismProperty API.

• mk: ∀ (n : ℕ), SSet.BoundaryInclusion (SSet.boundaryInclusion n)

def SSet.BoundaryInclusions : CategoryTheory.MorphismProperty SSet

The class of all boundary inclusions.

Equations

• SSet.BoundaryInclusions p = SSet.BoundaryInclusion p

def SSet.TrivialFibration : CategoryTheory.MorphismProperty SSet

a morphism of simplicial sets is a trivial fibration if it has the right lifting property wrt every boundary inclusion ∂Δ[n] ⟶ Δ[n].

Equations

• SSet.TrivialFibration p = SSet.BoundaryInclusions.rlp p

inductive SSet.InnerHornInclusion {X Y : SSet} : (X ⟶ Y) → Prop

Inductive definition of inner horn inclusions Λ[n, i] ⟶ Δ[n] by restricting general horn inclusions to 0 < i < n

• mk: ∀ (n i : ℕ), 0 < i → i < n → SSet.InnerHornInclusion (SSet.hornInclusion n ↑i)

def SSet.InnerHornInclusions : CategoryTheory.MorphismProperty SSet

The class of inner horn inclusions as a MorphismProperty

Equations

• SSet.InnerHornInclusions p = SSet.InnerHornInclusion p

inductive SSet.ZeroCoherentIsoInclusion {X Y : SSet} : (X ⟶ Y) → Prop

Inductive definition of being equal to the inclusion Δ[0] into coherent iso picking 0

• mk: SSet.ZeroCoherentIsoInclusion (SSet.coherentIso.pt CategoryTheory.WalkingIso.zero)

inductive SSet.OneCoherentIsoInclusion {X Y : SSet} : (X ⟶ Y) → Prop

Inductive definition of being equal to the inclusion Δ[0] into coherent iso picking 1

• mk: SSet.OneCoherentIsoInclusion (SSet.coherentIso.pt CategoryTheory.WalkingIso.one)

def SSet.IsZeroCoherentIsoInclusion : CategoryTheory.MorphismProperty SSet

The class of inclusions equal to the inclusion picking out zero in the coherent iso as a MorphismProperty

Equations

• SSet.IsZeroCoherentIsoInclusion p = SSet.ZeroCoherentIsoInclusion p

def SSet.IsOneCoherentIsoInclusion : CategoryTheory.MorphismProperty SSet

The class of inclusions equal to the inclusion picking out one in the coherent iso as a MorphismProperty

Equations

• SSet.IsOneCoherentIsoInclusion p = SSet.OneCoherentIsoInclusion p

def SSet.InnerHornIsoInclusion {X Y : SSet} (p : X ⟶ Y) : Prop

The union of inner horn inclusions and the two inclusions into coherent iso

Equations

• SSet.InnerHornIsoInclusion p = (SSet.InnerHornInclusions p ∨ SSet.IsZeroCoherentIsoInclusion p ∨ SSet.IsOneCoherentIsoInclusion p)

def SSet.InnerHornIsoInclusions : CategoryTheory.MorphismProperty SSet

The union of the class of inner horn inclusions and the inclusion into coherent iso as a MorphismProperty

Equations

• SSet.InnerHornIsoInclusions p = SSet.InnerHornIsoInclusion p

def SSet.IsoFibration : CategoryTheory.MorphismProperty SSet.QCat

Definition of isofibration: A simplicial map between quasi-categories is an \textbf{isofibration} if it lifts against the inner horn inclusions, as displayed below-left, and also against the inclusion of either vertex into the coherent isomorphism.

Equations

• SSet.IsoFibration p = SSet.InnerHornIsoInclusions.rlp p