@[reducible, inline]

abbrev SSet.Truncated.Edge.edgeMap {S : SSet} {y₀ y₁ : ((truncation 2).obj S).obj (Opposite.op { obj := SimplexCategory.mk 0, property := ⋯ })} (e : Edge y₀ y₁) : stdSimplex.obj (SimplexCategory.mk 1) ⟶ S

Equations

• e.edgeMap = SSet.yonedaEquiv.symm e.edge

class SSet.Truncated.Quasicategory₂ (X : Truncated 2) : Prop

A 2-truncated quasicategory is a 2-truncated simplicial set with 3 properties: (2, 1)-filling: any path of length 2 in may be filled to a 2-simplex whose spine equals the given path. (3, 1)-filling: given any path f of length 3, 2-simplices σ₃ and σ₀ filling the restricted paths f₀₁₂ and f₁₂₃ respectively, and a 2-simplex σ₂ filling the path formed by f₀₁ and the diagonal of σ₀, there is a 2-simplex σ₁ filling the path formed by the diagonal of σ₃ and f₂₃ and whose diagonal is the diagonal of σ₂. (3, 2)-filling: given any path f of length 3, 2-simplices σ₃ and σ₀ filling the restricted paths f₀₁₂ and f₁₂₃ respectively, and a 2-simplex σ₁ filling the path formed by f₂₃ and the diagonal of σ₃, there is a 2-simplex σ₂ filling the path formed by f₀₁ and the diagonal of σ₀ and whose diagonal is the diagonal of σ₁.

• fill21 {x₀ x₁ x₂ : X.obj (Opposite.op { obj := SimplexCategory.mk 0, property := ⋯ })} (e₀₁ : Edge x₀ x₁) (e₁₂ : Edge x₁ x₂) : Nonempty ((e₀₂ : Edge x₀ x₂) × e₀₁.CompStruct e₁₂ e₀₂)
• fill31 {x₀ x₁ x₂ x₃ : X.obj (Opposite.op { obj := SimplexCategory.mk 0, property := ⋯ })} {e₀₁ : Edge x₀ x₁} {e₁₂ : Edge x₁ x₂} {e₂₃ : Edge x₂ x₃} {e₀₂ : Edge x₀ x₂} {e₁₃ : Edge x₁ x₃} {e₀₃ : Edge x₀ x₃} (f₃ : e₀₁.CompStruct e₁₂ e₀₂) (f₀ : e₁₂.CompStruct e₂₃ e₁₃) (f₂ : e₀₁.CompStruct e₁₃ e₀₃) : Nonempty (e₀₂.CompStruct e₂₃ e₀₃)
• fill32 {x₀ x₁ x₂ x₃ : X.obj (Opposite.op { obj := SimplexCategory.mk 0, property := ⋯ })} {e₀₁ : Edge x₀ x₁} {e₁₂ : Edge x₁ x₂} {e₂₃ : Edge x₂ x₃} {e₀₂ : Edge x₀ x₂} {e₁₃ : Edge x₁ x₃} {e₀₃ : Edge x₀ x₃} (f₃ : e₀₁.CompStruct e₁₂ e₀₂) (f₀ : e₁₂.CompStruct e₂₃ e₁₃) (f₁ : e₀₂.CompStruct e₂₃ e₀₃) : Nonempty (e₀₁.CompStruct e₁₃ e₀₃)

theorem SSet.horn₂₁.path_edges_comm {S : SSet} {x₀ x₁ x₂ : ((truncation 2).obj S).obj (Opposite.op { obj := SimplexCategory.mk 0, property := ⋯ })} (e₀₁ : Truncated.Edge x₀ x₁) (e₁₂ : Truncated.Edge x₁ x₂) : CategoryTheory.CategoryStruct.comp pt₁ e₁₂.edgeMap = CategoryTheory.CategoryStruct.comp pt₀ e₀₁.edgeMap

def SSet.horn₂₁.fromEdges {S : SSet} {x₀ x₁ x₂ : ((truncation 2).obj S).obj (Opposite.op { obj := SimplexCategory.mk 0, property := ⋯ })} (e₀₁ : Truncated.Edge x₀ x₁) (e₁₂ : Truncated.Edge x₁ x₂) : (horn 2 1).toSSet ⟶ S

Given the data of two consecutive edges e₀₁ and e₁₂, construct a map Λ[2, 1].toSSet ⟶ S which restricts to maps Δ[1] ⟶ S corresponding to the two edges (this is made precise in the lemmas horn_from_edges_restr₀ and horn_from_edges_restr₁).

Equations

• SSet.horn₂₁.fromEdges e₀₁ e₁₂ = CategoryTheory.Limits.PushoutCocone.IsColimit.desc SSet.horn₂₁.pushoutIsPushout e₁₂.edgeMap e₀₁.edgeMap ⋯

theorem SSet.horn₂₁.horn_from_edges_restr₀ {S : SSet} {x₀ x₁ x₂ : ((truncation 2).obj S).obj (Opposite.op { obj := SimplexCategory.mk 0, property := ⋯ })} (e₀₁ : Truncated.Edge x₀ x₁) (e₁₂ : Truncated.Edge x₁ x₂) : CategoryTheory.CategoryStruct.comp ι₀ (fromEdges e₀₁ e₁₂) = yonedaEquiv.symm e₁₂.edge

See horn_from_edges for details.

theorem SSet.horn₂₁.horn_from_edges_restr₁ {S : SSet} {x₀ x₁ x₂ : ((truncation 2).obj S).obj (Opposite.op { obj := SimplexCategory.mk 0, property := ⋯ })} (e₀₁ : Truncated.Edge x₀ x₁) (e₁₂ : Truncated.Edge x₁ x₂) : CategoryTheory.CategoryStruct.comp ι₂ (fromEdges e₀₁ e₁₂) = yonedaEquiv.symm e₀₁.edge

See horn_from_edges for details.

def SSet.horn₂₁.fromHornExtension {S : SSet} {x₀ x₁ x₂ : ((truncation 2).obj S).obj (Opposite.op { obj := SimplexCategory.mk 0, property := ⋯ })} (e₀₁ : Truncated.Edge x₀ x₁) (e₁₂ : Truncated.Edge x₁ x₂) (g : stdSimplex.obj (SimplexCategory.mk 2) ⟶ S) (comm : fromEdges e₀₁ e₁₂ = CategoryTheory.CategoryStruct.comp (horn 2 1).ι g) : (e₀₂ : Truncated.Edge x₀ x₂) × e₀₁.CompStruct e₁₂ e₀₂

Given a map Δ[2] ⟶ S extending the horn given by horn_from_edges, construct and edge e₀₂ such that e₀₁, e₁₂, e₀₂ bound a 2-simplex of S (this is witnessed by CompStruct e₀₁ e₁₂ e₀₂).

Equations

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

def SSet.horn₃₁.chooseFace {S : SSet} {x₀ x₁ x₂ x₃ : ((truncation 2).obj S).obj (Opposite.op { obj := SimplexCategory.mk 0, property := ⋯ })} {e₀₁ : Truncated.Edge x₀ x₁} {e₁₂ : Truncated.Edge x₁ x₂} {e₂₃ : Truncated.Edge x₂ x₃} {e₀₂ : Truncated.Edge x₀ x₂} {e₁₃ : Truncated.Edge x₁ x₃} {e₀₃ : Truncated.Edge x₀ x₃} (f₃ : e₀₁.CompStruct e₁₂ e₀₂) (f₀ : e₁₂.CompStruct e₂₃ e₁₃) (f₂ : e₀₁.CompStruct e₁₃ e₀₃) (a : R) : stdSimplex.obj (SimplexCategory.mk 2) ⟶ S

Choose the i-th face from the given faces, where i is represented by a : horn₃₁.R, i.e. a is 0, 2 or 3

Equations

• SSet.horn₃₁.chooseFace f₃ f₀ f₂ SSet.horn₃₁.R.f₀ = SSet.yonedaEquiv.symm f₀.simplex
• SSet.horn₃₁.chooseFace f₃ f₀ f₂ SSet.horn₃₁.R.f₂ = SSet.yonedaEquiv.symm f₂.simplex
• SSet.horn₃₁.chooseFace f₃ f₀ f₂ SSet.horn₃₁.R.f₃ = SSet.yonedaEquiv.symm f₃.simplex

def SSet.horn₃₁.chooseFace' {S : SSet} {x₀ x₁ x₂ x₃ : ((truncation 2).obj S).obj (Opposite.op { obj := SimplexCategory.mk 0, property := ⋯ })} {e₀₁ : Truncated.Edge x₀ x₁} {e₁₂ : Truncated.Edge x₁ x₂} {e₂₃ : Truncated.Edge x₂ x₃} {e₀₂ : Truncated.Edge x₀ x₂} {e₁₃ : Truncated.Edge x₁ x₃} {e₀₃ : Truncated.Edge x₀ x₃} (f₃ : e₀₁.CompStruct e₁₂ e₀₂) (f₀ : e₁₂.CompStruct e₂₃ e₁₃) (f₂ : e₀₁.CompStruct e₁₃ e₀₃) (a : R) : S.obj (Opposite.op (SimplexCategory.mk 2))

Equations

• SSet.horn₃₁.chooseFace' f₃ f₀ f₂ SSet.horn₃₁.R.f₀ = f₀.simplex
• SSet.horn₃₁.chooseFace' f₃ f₀ f₂ SSet.horn₃₁.R.f₂ = f₂.simplex
• SSet.horn₃₁.chooseFace' f₃ f₀ f₂ SSet.horn₃₁.R.f₃ = f₃.simplex

def SSet.horn₃₁.multicoforkFromFaces {S : SSet} {x₀ x₁ x₂ x₃ : ((truncation 2).obj S).obj (Opposite.op { obj := SimplexCategory.mk 0, property := ⋯ })} {e₀₁ : Truncated.Edge x₀ x₁} {e₁₂ : Truncated.Edge x₁ x₂} {e₂₃ : Truncated.Edge x₂ x₃} {e₀₂ : Truncated.Edge x₀ x₂} {e₁₃ : Truncated.Edge x₁ x₃} {e₀₃ : Truncated.Edge x₀ x₃} (f₃ : e₀₁.CompStruct e₁₂ e₀₂) (f₀ : e₁₂.CompStruct e₂₃ e₁₃) (f₂ : e₀₁.CompStruct e₁₃ e₀₃) : CategoryTheory.Limits.Multicofork multispanIndex

Equations

• SSet.horn₃₁.multicoforkFromFaces f₃ f₀ f₂ = CategoryTheory.Limits.Multicofork.ofπ SSet.horn₃₁.multispanIndex S (SSet.horn₃₁.chooseFace f₃ f₀ f₂) ⋯

def SSet.horn₃₁.fromFaces {S : SSet} {x₀ x₁ x₂ x₃ : ((truncation 2).obj S).obj (Opposite.op { obj := SimplexCategory.mk 0, property := ⋯ })} {e₀₁ : Truncated.Edge x₀ x₁} {e₁₂ : Truncated.Edge x₁ x₂} {e₂₃ : Truncated.Edge x₂ x₃} {e₀₂ : Truncated.Edge x₀ x₂} {e₁₃ : Truncated.Edge x₁ x₃} {e₀₃ : Truncated.Edge x₀ x₃} (f₃ : e₀₁.CompStruct e₁₂ e₀₂) (f₀ : e₁₂.CompStruct e₂₃ e₁₃) (f₂ : e₀₁.CompStruct e₁₃ e₀₃) : (horn 3 1).toSSet ⟶ S

Use the fact that Λ[3, 1] is the coequalizer of multicoforkFromFaces allows the construction of a map Λ[3, 1].toSSet ⟶ S.

Equations

• SSet.horn₃₁.fromFaces f₃ f₀ f₂ = SSet.horn₃₁.isMulticoeq.desc (SSet.horn₃₁.multicoforkFromFaces f₃ f₀ f₂)

theorem SSet.horn₃₁.horn_extension_face₀ {S : SSet} {x₀ x₁ x₂ x₃ : ((truncation 2).obj S).obj (Opposite.op { obj := SimplexCategory.mk 0, property := ⋯ })} {e₀₁ : Truncated.Edge x₀ x₁} {e₁₂ : Truncated.Edge x₁ x₂} {e₂₃ : Truncated.Edge x₂ x₃} {e₀₂ : Truncated.Edge x₀ x₂} {e₁₃ : Truncated.Edge x₁ x₃} {e₀₃ : Truncated.Edge x₀ x₃} (f₃ : e₀₁.CompStruct e₁₂ e₀₂) (f₀ : e₁₂.CompStruct e₂₃ e₁₃) (f₂ : e₀₁.CompStruct e₁₃ e₀₃) {g : stdSimplex.obj (SimplexCategory.mk 3) ⟶ S} (comm : fromFaces f₃ f₀ f₂ = CategoryTheory.CategoryStruct.comp (horn 3 1).ι g) : yonedaEquiv.symm f₀.simplex = CategoryTheory.CategoryStruct.comp (stdSimplex.δ 0) g

theorem SSet.horn₃₁.horn_extension_face₂ {S : SSet} {x₀ x₁ x₂ x₃ : ((truncation 2).obj S).obj (Opposite.op { obj := SimplexCategory.mk 0, property := ⋯ })} {e₀₁ : Truncated.Edge x₀ x₁} {e₁₂ : Truncated.Edge x₁ x₂} {e₂₃ : Truncated.Edge x₂ x₃} {e₀₂ : Truncated.Edge x₀ x₂} {e₁₃ : Truncated.Edge x₁ x₃} {e₀₃ : Truncated.Edge x₀ x₃} (f₃ : e₀₁.CompStruct e₁₂ e₀₂) (f₀ : e₁₂.CompStruct e₂₃ e₁₃) (f₂ : e₀₁.CompStruct e₁₃ e₀₃) {g : stdSimplex.obj (SimplexCategory.mk 3) ⟶ S} (comm : fromFaces f₃ f₀ f₂ = CategoryTheory.CategoryStruct.comp (horn 3 1).ι g) : yonedaEquiv.symm f₂.simplex = CategoryTheory.CategoryStruct.comp (stdSimplex.δ 2) g

theorem SSet.horn₃₁.horn_extension_face₃ {S : SSet} {x₀ x₁ x₂ x₃ : ((truncation 2).obj S).obj (Opposite.op { obj := SimplexCategory.mk 0, property := ⋯ })} {e₀₁ : Truncated.Edge x₀ x₁} {e₁₂ : Truncated.Edge x₁ x₂} {e₂₃ : Truncated.Edge x₂ x₃} {e₀₂ : Truncated.Edge x₀ x₂} {e₁₃ : Truncated.Edge x₁ x₃} {e₀₃ : Truncated.Edge x₀ x₃} (f₃ : e₀₁.CompStruct e₁₂ e₀₂) (f₀ : e₁₂.CompStruct e₂₃ e₁₃) (f₂ : e₀₁.CompStruct e₁₃ e₀₃) {g : stdSimplex.obj (SimplexCategory.mk 3) ⟶ S} (comm : fromFaces f₃ f₀ f₂ = CategoryTheory.CategoryStruct.comp (horn 3 1).ι g) : yonedaEquiv.symm f₃.simplex = CategoryTheory.CategoryStruct.comp (stdSimplex.δ 3) g

def SSet.horn₃₁.fromHornExtension {S : SSet} {x₀ x₁ x₂ x₃ : ((truncation 2).obj S).obj (Opposite.op { obj := SimplexCategory.mk 0, property := ⋯ })} {e₀₁ : Truncated.Edge x₀ x₁} {e₁₂ : Truncated.Edge x₁ x₂} {e₂₃ : Truncated.Edge x₂ x₃} {e₀₂ : Truncated.Edge x₀ x₂} {e₁₃ : Truncated.Edge x₁ x₃} {e₀₃ : Truncated.Edge x₀ x₃} (f₃ : e₀₁.CompStruct e₁₂ e₀₂) (f₀ : e₁₂.CompStruct e₂₃ e₁₃) (f₂ : e₀₁.CompStruct e₁₃ e₀₃) (g : stdSimplex.obj (SimplexCategory.mk 3) ⟶ S) (comm : fromFaces f₃ f₀ f₂ = CategoryTheory.CategoryStruct.comp (horn 3 1).ι g) : e₀₂.CompStruct e₂₃ e₀₃

Given a map Δ[3] ⟶ S extending the horn given by fromFaces, obtain a 2-simplex bounded by edges e₀₂, e₂₃ and e₀₃. See also Quasicategory₂.fill31.

Equations

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

def SSet.horn₃₂.chooseFace {S : SSet} {x₀ x₁ x₂ x₃ : ((truncation 2).obj S).obj (Opposite.op { obj := SimplexCategory.mk 0, property := ⋯ })} {e₀₁ : Truncated.Edge x₀ x₁} {e₁₂ : Truncated.Edge x₁ x₂} {e₂₃ : Truncated.Edge x₂ x₃} {e₀₂ : Truncated.Edge x₀ x₂} {e₁₃ : Truncated.Edge x₁ x₃} {e₀₃ : Truncated.Edge x₀ x₃} (f₃ : e₀₁.CompStruct e₁₂ e₀₂) (f₀ : e₁₂.CompStruct e₂₃ e₁₃) (f₁ : e₀₂.CompStruct e₂₃ e₀₃) (a : R) : stdSimplex.obj (SimplexCategory.mk 2) ⟶ S

Choose the i-th face from the given faces, where i is represented by a : horn₃₂.R, i.e. a is 0, 1 or 3

Equations

• SSet.horn₃₂.chooseFace f₃ f₀ f₁ SSet.horn₃₂.R.f₀ = SSet.yonedaEquiv.symm f₀.simplex
• SSet.horn₃₂.chooseFace f₃ f₀ f₁ SSet.horn₃₂.R.f₁ = SSet.yonedaEquiv.symm f₁.simplex
• SSet.horn₃₂.chooseFace f₃ f₀ f₁ SSet.horn₃₂.R.f₃ = SSet.yonedaEquiv.symm f₃.simplex

def SSet.horn₃₂.chooseFace' {S : SSet} {x₀ x₁ x₂ x₃ : ((truncation 2).obj S).obj (Opposite.op { obj := SimplexCategory.mk 0, property := ⋯ })} {e₀₁ : Truncated.Edge x₀ x₁} {e₁₂ : Truncated.Edge x₁ x₂} {e₂₃ : Truncated.Edge x₂ x₃} {e₀₂ : Truncated.Edge x₀ x₂} {e₁₃ : Truncated.Edge x₁ x₃} {e₀₃ : Truncated.Edge x₀ x₃} (f₃ : e₀₁.CompStruct e₁₂ e₀₂) (f₀ : e₁₂.CompStruct e₂₃ e₁₃) (f₁ : e₀₂.CompStruct e₂₃ e₀₃) (a : R) : S.obj (Opposite.op (SimplexCategory.mk 2))

Equations

• SSet.horn₃₂.chooseFace' f₃ f₀ f₁ SSet.horn₃₂.R.f₀ = f₀.simplex
• SSet.horn₃₂.chooseFace' f₃ f₀ f₁ SSet.horn₃₂.R.f₁ = f₁.simplex
• SSet.horn₃₂.chooseFace' f₃ f₀ f₁ SSet.horn₃₂.R.f₃ = f₃.simplex

def SSet.horn₃₂.multicoforkFromFaces {S : SSet} {x₀ x₁ x₂ x₃ : ((truncation 2).obj S).obj (Opposite.op { obj := SimplexCategory.mk 0, property := ⋯ })} {e₀₁ : Truncated.Edge x₀ x₁} {e₁₂ : Truncated.Edge x₁ x₂} {e₂₃ : Truncated.Edge x₂ x₃} {e₀₂ : Truncated.Edge x₀ x₂} {e₁₃ : Truncated.Edge x₁ x₃} {e₀₃ : Truncated.Edge x₀ x₃} (f₃ : e₀₁.CompStruct e₁₂ e₀₂) (f₀ : e₁₂.CompStruct e₂₃ e₁₃) (f₁ : e₀₂.CompStruct e₂₃ e₀₃) : CategoryTheory.Limits.Multicofork multispanIndex

Equations

• SSet.horn₃₂.multicoforkFromFaces f₃ f₀ f₁ = CategoryTheory.Limits.Multicofork.ofπ SSet.horn₃₂.multispanIndex S (SSet.horn₃₂.chooseFace f₃ f₀ f₁) ⋯

def SSet.horn₃₂.fromFaces {S : SSet} {x₀ x₁ x₂ x₃ : ((truncation 2).obj S).obj (Opposite.op { obj := SimplexCategory.mk 0, property := ⋯ })} {e₀₁ : Truncated.Edge x₀ x₁} {e₁₂ : Truncated.Edge x₁ x₂} {e₂₃ : Truncated.Edge x₂ x₃} {e₀₂ : Truncated.Edge x₀ x₂} {e₁₃ : Truncated.Edge x₁ x₃} {e₀₃ : Truncated.Edge x₀ x₃} (f₃ : e₀₁.CompStruct e₁₂ e₀₂) (f₀ : e₁₂.CompStruct e₂₃ e₁₃) (f₁ : e₀₂.CompStruct e₂₃ e₀₃) : (horn 3 2).toSSet ⟶ S

Use the fact that Λ[3, 2] is the coequalizer of multicoforkFromFaces allows the construction of a map Λ[3, 2].toSSet ⟶ S.

Equations

• SSet.horn₃₂.fromFaces f₃ f₀ f₁ = SSet.horn₃₂.multicoforkIsMulticoeq.desc (SSet.horn₃₂.multicoforkFromFaces f₃ f₀ f₁)

theorem SSet.horn₃₂.horn_extension_face₀ {S : SSet} {x₀ x₁ x₂ x₃ : ((truncation 2).obj S).obj (Opposite.op { obj := SimplexCategory.mk 0, property := ⋯ })} {e₀₁ : Truncated.Edge x₀ x₁} {e₁₂ : Truncated.Edge x₁ x₂} {e₂₃ : Truncated.Edge x₂ x₃} {e₀₂ : Truncated.Edge x₀ x₂} {e₁₃ : Truncated.Edge x₁ x₃} {e₀₃ : Truncated.Edge x₀ x₃} (f₃ : e₀₁.CompStruct e₁₂ e₀₂) (f₀ : e₁₂.CompStruct e₂₃ e₁₃) (f₁ : e₀₂.CompStruct e₂₃ e₀₃) {g : stdSimplex.obj (SimplexCategory.mk 3) ⟶ S} (comm : fromFaces f₃ f₀ f₁ = CategoryTheory.CategoryStruct.comp (horn 3 2).ι g) : yonedaEquiv.symm f₀.simplex = CategoryTheory.CategoryStruct.comp (stdSimplex.δ 0) g

theorem SSet.horn₃₂.horn_extension_face₁ {S : SSet} {x₀ x₁ x₂ x₃ : ((truncation 2).obj S).obj (Opposite.op { obj := SimplexCategory.mk 0, property := ⋯ })} {e₀₁ : Truncated.Edge x₀ x₁} {e₁₂ : Truncated.Edge x₁ x₂} {e₂₃ : Truncated.Edge x₂ x₃} {e₀₂ : Truncated.Edge x₀ x₂} {e₁₃ : Truncated.Edge x₁ x₃} {e₀₃ : Truncated.Edge x₀ x₃} (f₃ : e₀₁.CompStruct e₁₂ e₀₂) (f₀ : e₁₂.CompStruct e₂₃ e₁₃) (f₁ : e₀₂.CompStruct e₂₃ e₀₃) {g : stdSimplex.obj (SimplexCategory.mk 3) ⟶ S} (comm : fromFaces f₃ f₀ f₁ = CategoryTheory.CategoryStruct.comp (horn 3 2).ι g) : yonedaEquiv.symm f₁.simplex = CategoryTheory.CategoryStruct.comp (stdSimplex.δ 1) g

theorem SSet.horn₃₂.horn_extension_face₃ {S : SSet} {x₀ x₁ x₂ x₃ : ((truncation 2).obj S).obj (Opposite.op { obj := SimplexCategory.mk 0, property := ⋯ })} {e₀₁ : Truncated.Edge x₀ x₁} {e₁₂ : Truncated.Edge x₁ x₂} {e₂₃ : Truncated.Edge x₂ x₃} {e₀₂ : Truncated.Edge x₀ x₂} {e₁₃ : Truncated.Edge x₁ x₃} {e₀₃ : Truncated.Edge x₀ x₃} (f₃ : e₀₁.CompStruct e₁₂ e₀₂) (f₀ : e₁₂.CompStruct e₂₃ e₁₃) (f₁ : e₀₂.CompStruct e₂₃ e₀₃) {g : stdSimplex.obj (SimplexCategory.mk 3) ⟶ S} (comm : fromFaces f₃ f₀ f₁ = CategoryTheory.CategoryStruct.comp (horn 3 2).ι g) : yonedaEquiv.symm f₃.simplex = CategoryTheory.CategoryStruct.comp (stdSimplex.δ 3) g

def SSet.horn₃₂.fromHornExtension {S : SSet} {x₀ x₁ x₂ x₃ : ((truncation 2).obj S).obj (Opposite.op { obj := SimplexCategory.mk 0, property := ⋯ })} {e₀₁ : Truncated.Edge x₀ x₁} {e₁₂ : Truncated.Edge x₁ x₂} {e₂₃ : Truncated.Edge x₂ x₃} {e₀₂ : Truncated.Edge x₀ x₂} {e₁₃ : Truncated.Edge x₁ x₃} {e₀₃ : Truncated.Edge x₀ x₃} (f₃ : e₀₁.CompStruct e₁₂ e₀₂) (f₀ : e₁₂.CompStruct e₂₃ e₁₃) (f₁ : e₀₂.CompStruct e₂₃ e₀₃) (g : stdSimplex.obj (SimplexCategory.mk 3) ⟶ S) (comm : fromFaces f₃ f₀ f₁ = CategoryTheory.CategoryStruct.comp (horn 3 2).ι g) : e₀₁.CompStruct e₁₃ e₀₃

Given a map Δ[3] ⟶ S extending the horn given by fromFaces, obtain a 2-simplex bounded by edges e₀₁, e₁₃ and e₀₃. See also Quasicategory₂.fill32.

Equations

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

instance SSet.Truncated.two_truncatation_of_qc_is_2_trunc_qc {X : SSet} [X.Quasicategory] : ((truncation 2).obj X).Quasicategory₂

The 2-truncation of a quasi-category is a 2-truncated quasi-category.

def SSet.Truncated.Edge.CompStruct.idCompId {A : Truncated 2} (x : A.obj (Opposite.op { obj := SimplexCategory.mk 0, property := ⋯ })) : (id x).CompStruct (id x) (id x)

Equations

• SSet.Truncated.Edge.CompStruct.idCompId x = SSet.Truncated.Edge.CompStruct.compId (SSet.Truncated.Edge.id x)

@[reducible, inline]

abbrev SSet.Truncated.HomotopicL {A : Truncated 2} {x y : A.obj (Opposite.op { obj := SimplexCategory.mk 0, property := ⋯ })} (f g : Edge x y) : Prop

Two edges f and g are left homotopic if there is a 2-simplex with (0, 1)-edge f, (0, 2)-edge g and (1, 2)-edge id. We use Nonempty to have a Prop valued HomotopicL.

Equations

• SSet.Truncated.HomotopicL f g = Nonempty (f.CompStruct (SSet.Truncated.Edge.id y) g)

@[reducible, inline]

abbrev SSet.Truncated.HomotopicR {A : Truncated 2} {x y : A.obj (Opposite.op { obj := SimplexCategory.mk 0, property := ⋯ })} (f g : Edge x y) : Prop

Two edges f and g are right homotopic if there is a 2-simplex with (0, 1)-edge id, (0, 2)-edge g and (1, 2)-edge f. We use Nonempty to have a Prop valued HomotopicL.

Equations

• SSet.Truncated.HomotopicR f g = Nonempty ((SSet.Truncated.Edge.id x).CompStruct f g)

def SSet.Quasicategory₂.HomotopicL.refl {A : Truncated 2} {x y : A.obj (Opposite.op { obj := SimplexCategory.mk 0, property := ⋯ })} {f : Truncated.Edge x y} : Truncated.HomotopicL f f

Left homotopy relation is reflexive

Equations

• ⋯ = ⋯

def SSet.Quasicategory₂.HomotopicL.symm {A : Truncated 2} [A.Quasicategory₂] {x y : A.obj (Opposite.op { obj := SimplexCategory.mk 0, property := ⋯ })} {f g : Truncated.Edge x y} (hfg : Truncated.HomotopicL f g) : Truncated.HomotopicL g f

Left homotopy relation is symmetric

Equations

• ⋯ = ⋯

def SSet.Quasicategory₂.HomotopicL.trans {A : Truncated 2} [A.Quasicategory₂] {x y : A.obj (Opposite.op { obj := SimplexCategory.mk 0, property := ⋯ })} {f g h : Truncated.Edge x y} (hfg : Truncated.HomotopicL f g) (hgh : Truncated.HomotopicL g h) : Truncated.HomotopicL f h

Left homotopy relation is transitive

Equations

• ⋯ = ⋯

def SSet.Quasicategory₂.HomotopicR.refl {A : Truncated 2} {x y : A.obj (Opposite.op { obj := SimplexCategory.mk 0, property := ⋯ })} {f : Truncated.Edge x y} : Truncated.HomotopicR f f

Right homotopy relation is reflexive

Equations

• ⋯ = ⋯

def SSet.Quasicategory₂.HomotopicR.symm {A : Truncated 2} [A.Quasicategory₂] {x y : A.obj (Opposite.op { obj := SimplexCategory.mk 0, property := ⋯ })} {f g : Truncated.Edge x y} (hfg : Truncated.HomotopicR f g) : Truncated.HomotopicR g f

Right homotopy relation is symmetric

Equations

• ⋯ = ⋯

def SSet.Quasicategory₂.HomotopicR.trans {A : Truncated 2} [A.Quasicategory₂] {x y : A.obj (Opposite.op { obj := SimplexCategory.mk 0, property := ⋯ })} {f g h : Truncated.Edge x y} (hfg : Truncated.HomotopicR f g) (hgh : Truncated.HomotopicR g h) : Truncated.HomotopicR f h

Right homotopy relation is transitive

Equations

• ⋯ = ⋯

theorem SSet.Quasicategory₂.HomotopicL_iff_HomotopicR {A : Truncated 2} [A.Quasicategory₂] {x y : A.obj (Opposite.op { obj := SimplexCategory.mk 0, property := ⋯ })} {f g : Truncated.Edge x y} : Truncated.HomotopicL f g ↔ Truncated.HomotopicR f g

The right and left homotopy relations coincide

theorem SSet.Quasicategory₂.comp_unique {A : Truncated 2} [A.Quasicategory₂] {x y z : A.obj (Opposite.op { obj := SimplexCategory.mk 0, property := ⋯ })} {f : Truncated.Edge x y} {g : Truncated.Edge y z} {h h' : Truncated.Edge x z} (s : f.CompStruct g h) (s' : f.CompStruct g h') : Truncated.HomotopicL h h'

theorem SSet.Quasicategory₂.comp_unique' {A : Truncated 2} [A.Quasicategory₂] {x y z : A.obj (Opposite.op { obj := SimplexCategory.mk 0, property := ⋯ })} {f : Truncated.Edge x y} {g : Truncated.Edge y z} {h h' : Truncated.Edge x z} (s : Nonempty (f.CompStruct g h)) (s' : Nonempty (f.CompStruct g h')) : Truncated.HomotopicL h h'

theorem SSet.Quasicategory₂.transport_edge₀ {A : Truncated 2} [A.Quasicategory₂] {x y z : A.obj (Opposite.op { obj := SimplexCategory.mk 0, property := ⋯ })} {f : Truncated.Edge x y} {g g' : Truncated.Edge y z} {h : Truncated.Edge x z} (s : f.CompStruct g h) (htpy : Truncated.HomotopicL g g') : Nonempty (f.CompStruct g' h)

theorem SSet.Quasicategory₂.transport_edge₁ {A : Truncated 2} [A.Quasicategory₂] {x y z : A.obj (Opposite.op { obj := SimplexCategory.mk 0, property := ⋯ })} {f : Truncated.Edge x y} {g : Truncated.Edge y z} {h h' : Truncated.Edge x z} (s : f.CompStruct g h) (htpy : Truncated.HomotopicL h h') : Nonempty (f.CompStruct g h')

theorem SSet.Quasicategory₂.transport_edge₂ {A : Truncated 2} [A.Quasicategory₂] {x y z : A.obj (Opposite.op { obj := SimplexCategory.mk 0, property := ⋯ })} {f f' : Truncated.Edge x y} {g : Truncated.Edge y z} {h : Truncated.Edge x z} (s : f.CompStruct g h) (htpy : Truncated.HomotopicL f f') : Nonempty (f'.CompStruct g h)

theorem SSet.Quasicategory₂.transport_all_edges {A : Truncated 2} [A.Quasicategory₂] {x y z : A.obj (Opposite.op { obj := SimplexCategory.mk 0, property := ⋯ })} {f f' : Truncated.Edge x y} {g g' : Truncated.Edge y z} {h h' : Truncated.Edge x z} (hf : Truncated.HomotopicL f f') (hg : Truncated.HomotopicL g g') (hh : Truncated.HomotopicL h h') (s : f.CompStruct g h) : Nonempty (f'.CompStruct g' h')

def SSet.Quasicategory₂.HomotopyCategory₂ (A : Truncated 2) : Type u_1

The homotopy category of a 2-truncated quasicategory A has as objects the 0-simplices of A

Equations

• SSet.Quasicategory₂.HomotopyCategory₂ A = A.obj (Opposite.op { obj := SimplexCategory.mk 0, property := SSet.Truncated.Edge.edgeMap._proof_1 })

instance SSet.Quasicategory₂.instSetoidEdge {A : Truncated 2} [A.Quasicategory₂] (x₀ x₁ : A.obj (Opposite.op { obj := SimplexCategory.mk 0, property := ⋯ })) : Setoid (Truncated.Edge x₀ x₁)

Equations

• SSet.Quasicategory₂.instSetoidEdge x₀ x₁ = { r := SSet.Truncated.HomotopicL, iseqv := ⋯ }

def SSet.Quasicategory₂.HEdge {A : Truncated 2} [A.Quasicategory₂] (x₀ x₁ : A.obj (Opposite.op { obj := SimplexCategory.mk 0, property := ⋯ })) : Type u_1

The morphisms between two vertices x₀, x₁ in HomotopyCategory₂ A are homotopy classes of 1-simplices between x₀ and x₁.

Equations

• SSet.Quasicategory₂.HEdge x₀ x₁ = Quotient (SSet.Quasicategory₂.instSetoidEdge x₀ x₁)

noncomputable def SSet.Quasicategory₂.composeEdges {A : Truncated 2} [A.Quasicategory₂] {x₀ x₁ x₂ : A.obj (Opposite.op { obj := SimplexCategory.mk 0, property := ⋯ })} (f : Truncated.Edge x₀ x₁) (g : Truncated.Edge x₁ x₂) : Truncated.Edge x₀ x₂

Given two consecutive edges f, g in a 2-truncated quasicategory, nonconstructively choose an edge that is the diagonal of a 2-simplex with spine given by f and g.

Equations

• SSet.Quasicategory₂.composeEdges f g = ⋯.some.fst

noncomputable def SSet.Quasicategory₂.composeEdgesIsComposition {A : Truncated 2} [A.Quasicategory₂] {x₀ x₁ x₂ : A.obj (Opposite.op { obj := SimplexCategory.mk 0, property := ⋯ })} (f : Truncated.Edge x₀ x₁) (g : Truncated.Edge x₁ x₂) : f.CompStruct g (composeEdges f g)

Equations

• SSet.Quasicategory₂.composeEdgesIsComposition f g = ⋯.some.snd

theorem SSet.Quasicategory₂.composeEdges_unique {A : Truncated 2} [A.Quasicategory₂] {x₀ x₁ x₂ : A.obj (Opposite.op { obj := SimplexCategory.mk 0, property := ⋯ })} {f : Truncated.Edge x₀ x₁} {g : Truncated.Edge x₁ x₂} {h : Truncated.Edge x₀ x₂} (s : f.CompStruct g h) : Truncated.HomotopicL h (composeEdges f g)

The edge composeEdges f g is the unique edge up to homotopy such that there is a 2-simplex with spine given by f and g.

theorem SSet.Quasicategory₂.composeEdges_homotopic {A : Truncated 2} [A.Quasicategory₂] {x₀ x₁ x₂ : A.obj (Opposite.op { obj := SimplexCategory.mk 0, property := ⋯ })} {f f' : Truncated.Edge x₀ x₁} {g g' : Truncated.Edge x₁ x₂} (hf : Truncated.HomotopicL f f') (hg : Truncated.HomotopicL g g') : Truncated.HomotopicL (composeEdges f g) (composeEdges f' g')

The compositions of homotopic edges are homotopic

noncomputable def SSet.Quasicategory₂.composeHEdges {A : Truncated 2} [A.Quasicategory₂] {x₀ x₁ x₂ : A.obj (Opposite.op { obj := SimplexCategory.mk 0, property := ⋯ })} (f : HEdge x₀ x₁) (g : HEdge x₁ x₂) : HEdge x₀ x₂

Composition of morphisms in HomotopyCategory₂ A is given by lifting composeEdges.

Equations

• SSet.Quasicategory₂.composeHEdges f g = Quotient.lift₂ (fun (f : SSet.Truncated.Edge x₀ x₁) (g : SSet.Truncated.Edge x₁ x₂) => ⟦SSet.Quasicategory₂.composeEdges f g⟧) ⋯ f g

noncomputable instance SSet.Quasicategory₂.instCategoryStructHomotopyCategory₂ {A : Truncated 2} [A.Quasicategory₂] : CategoryTheory.CategoryStruct.{u_1, u_1} (HomotopyCategory₂ A)

Equations

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

noncomputable instance SSet.Quasicategory₂.instCategoryHomotopyCategory₂ {A : Truncated 2} [A.Quasicategory₂] : CategoryTheory.Category.{u_1, u_1} (HomotopyCategory₂ A)

Equations

• SSet.Quasicategory₂.instCategoryHomotopyCategory₂ = { toCategoryStruct := SSet.Quasicategory₂.instCategoryStructHomotopyCategory₂, id_comp := ⋯, comp_id := ⋯, assoc := ⋯ }

noncomputable def SSet.Quasicategory₂.quotientReflPrefunctor₂ {A : Truncated 2} [A.Quasicategory₂] : OneTruncation₂ A ⥤rq HomotopyCategory₂ A

The reflexive prefunctor sending edges (in the 1-truncation) of A to their homotopy class.

Equations

• SSet.Quasicategory₂.quotientReflPrefunctor₂ = { obj := id, map := fun {X Y : SSet.OneTruncation₂ A} (f : X ⟶ Y) => Quotient.mk' { edge := f.edge, src_eq := ⋯, tgt_eq := ⋯ }, map_id := ⋯ }

noncomputable def SSet.Quasicategory₂.quotientFunctor₂ {A : Truncated 2} [A.Quasicategory₂] : CategoryTheory.Functor (CategoryTheory.Cat.FreeRefl (OneTruncation₂ A)) (HomotopyCategory₂ A)

By the adjunction ReflQuiv.adj, we obtain a functor from the free category on the reflexive quiver underlying A to the homotopy category corresponding to quotientReflPrefunctor₂.

Equations

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

theorem SSet.Quasicategory₂.unit_app_quotientFunctor {A : Truncated 2} [A.Quasicategory₂] : quotientReflPrefunctor₂ = CategoryTheory.ReflQuiv.adj.unit.app (OneTruncation₂ A) ⋙rq quotientFunctor₂.toReflPrefunctor

The adjoint relation between quotientReflPrefunctor₂ and quotientFunctor₂ expressed on the level of functors.

theorem SSet.Quasicategory₂.quotientFunctor_obj {A : Truncated 2} [A.Quasicategory₂] (x : CategoryTheory.Cat.FreeRefl (OneTruncation₂ A)) : quotientFunctor₂.obj x = x.as

theorem SSet.Quasicategory₂.qFunctor_map_toPath {A : Truncated 2} [A.Quasicategory₂] (x y : CategoryTheory.Cat.FreeRefl (OneTruncation₂ A)) (f : OneTruncation₂.Hom x.as y.as) : quotientFunctor₂.map (Quot.mk (CategoryTheory.Quotient.CompClosure CategoryTheory.Cat.FreeReflRel) (Quiver.Hom.toPath f)) = quotientReflPrefunctor₂.map f

theorem SSet.Quasicategory₂.qFunctor_map_path {A : Truncated 2} [A.Quasicategory₂] {x y : OneTruncation₂ A} (p : Quiver.Path x y) : quotientFunctor₂.map (Quot.mk (CategoryTheory.Quotient.CompClosure CategoryTheory.Cat.FreeReflRel) p) = (CategoryTheory.ReflQuiv.adj.counit.app (HomotopyCategory₂ A)).map (Quot.mk (CategoryTheory.Quotient.CompClosure CategoryTheory.Cat.FreeReflRel) (quotientReflPrefunctor₂.mapPath p))

theorem SSet.Quasicategory₂.qFunctor_respects_horel₂ {A : Truncated 2} [A.Quasicategory₂] (x y : CategoryTheory.Cat.FreeRefl (OneTruncation₂ A)) (f g : x ⟶ y) (r : Truncated.HoRel₂ x y f g) : quotientFunctor₂.map f = quotientFunctor₂.map g

quotientFunctor₂ respects the hom relation HoRel₂.

def SSet.Quasicategory₂.edgeToHom {A : Truncated 2} {x₀ x₁ : A.obj (Opposite.op { obj := SimplexCategory.mk 0, property := ⋯ })} (f : Truncated.Edge x₀ x₁) : x₀ ⟶ x₁

An edge from x₀ to x₁ in a 2-truncated simplicial set defines an arrow in the refl quiver OneTruncation₂.{u} A) from x₀ to x₁.

Equations

• SSet.Quasicategory₂.edgeToHom f = { edge := f.edge, src_eq := ⋯, tgt_eq := ⋯ }

def SSet.Quasicategory₂.edgeToFreeHom {A : Truncated 2} {x₀ x₁ : A.obj (Opposite.op { obj := SimplexCategory.mk 0, property := ⋯ })} (f : Truncated.Edge x₀ x₁) : { as := x₀ } ⟶ { as := x₁ }

An edge from x₀ to x₁ in a 2-truncated simplicial set defines an arrow in the free category generated from the refl quiver OneTruncation₂.{u} A) from x₀ to x₁.

Equations

• SSet.Quasicategory₂.edgeToFreeHom f = Quot.mk (CategoryTheory.Quotient.CompClosure CategoryTheory.Cat.FreeReflRel) (SSet.Quasicategory₂.edgeToHom f).toPath

theorem SSet.Quasicategory₂.compose_id_path {A : Truncated 2} {x₀ x₁ : A.obj (Opposite.op { obj := SimplexCategory.mk 0, property := ⋯ })} (f : Truncated.Edge x₀ x₁) : edgeToFreeHom f = Quot.mk (CategoryTheory.Quotient.CompClosure CategoryTheory.Cat.FreeReflRel) ((edgeToHom f).toPath.comp (edgeToHom (Truncated.Edge.id x₁)).toPath)

theorem SSet.Quasicategory₂.homotopic_edges_are_equiv {A : Truncated 2} [A.Quasicategory₂] {x₀ x₁ : A.obj (Opposite.op { obj := SimplexCategory.mk 0, property := ⋯ })} (f g : Truncated.Edge x₀ x₁) (htpy : Truncated.HomotopicL f g) : Truncated.HoRel₂ { as := x₀ } { as := x₁ } (edgeToFreeHom f) (edgeToFreeHom g)

Two (left) homotopic edges f, g are equivalent under the hom-relation HoRel₂ generated by 2-simplices.

noncomputable def SSet.Quasicategory₂.liftRq₂ {A : Truncated 2} [A.Quasicategory₂] {C : Type} [CategoryTheory.ReflQuiver C] (F : CategoryTheory.Cat.FreeRefl (OneTruncation₂ A) ⥤rq C) (h : ∀ (x y : CategoryTheory.Cat.FreeRefl (OneTruncation₂ A)) (f g : x ⟶ y), Truncated.HoRel₂ x y f g → F.map f = F.map g) : HomotopyCategory₂ A ⥤rq C

If a reflexive prefunctor F : FreeRefl (OneTruncation₂ A) ⥤rq C respects the hom-relation HoRel₂, then it can be lifted to HomotopyCategory₂ A.

Equations

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

theorem SSet.Quasicategory₂.lift_unique_rq₂ {A : Truncated 2} [A.Quasicategory₂] {C : Type u} [CategoryTheory.ReflQuiver C] (F₁ F₂ : HomotopyCategory₂ A ⥤rq C) (h : quotientReflPrefunctor₂ ⋙rq F₁ = quotientReflPrefunctor₂ ⋙rq F₂) : F₁ = F₂

noncomputable def SSet.Quasicategory₂.lift₂ {A : Truncated 2} [A.Quasicategory₂] {C : Type} [CategoryTheory.Category.{u_1, 0} C] (F : CategoryTheory.Functor (CategoryTheory.Cat.FreeRefl (OneTruncation₂ A)) C) (h : ∀ (x y : CategoryTheory.Cat.FreeRefl (OneTruncation₂ A)) (f g : x ⟶ y), Truncated.HoRel₂ x y f g → F.map f = F.map g) : CategoryTheory.Functor (HomotopyCategory₂ A) C

If a functor F : FreeRefl (OneTruncation₂ A) ⥤ C respects the hom-relation HoRel₂, then it can be lifted to HomotopyCategory₂ A (see the weaker statement liftRq₂).

Equations

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

theorem SSet.Quasicategory₂.is_lift₂ {A : Truncated 2} [A.Quasicategory₂] {C : Type} [CategoryTheory.Category.{u_1, 0} C] (F : CategoryTheory.Functor (CategoryTheory.Cat.FreeRefl (OneTruncation₂ A)) C) (h : ∀ (x y : CategoryTheory.Cat.FreeRefl (OneTruncation₂ A)) (f g : x ⟶ y), Truncated.HoRel₂ x y f g → F.map f = F.map g) : quotientFunctor₂.comp (lift₂ F h) = F

theorem SSet.Quasicategory₂.HomotopyCategory₂.lift_unique' {A : Truncated 2} [A.Quasicategory₂] {C : Type u} [CategoryTheory.Category.{u, u} C] (F₁ F₂ : CategoryTheory.Functor (HomotopyCategory₂ A) C) (h : quotientFunctor₂.comp F₁ = quotientFunctor₂.comp F₂) : F₁ = F₂

Lifts to the homotopy category are unique.

noncomputable def SSet.Quasicategory₂.isoHomotopyCategories {A : Truncated 2} [A.Quasicategory₂] : CategoryTheory.Cat.of A.HomotopyCategory ≅ CategoryTheory.Cat.of (HomotopyCategory₂ A)

Since both HomotopyCategory A and HomotopyCategory₂ A satisfy the same universal property, they are isomorphic.

Equations

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