@[reducible, inline]

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

Equations

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

theorem SSet.horn₂₁.incl₀ : CategoryTheory.CategoryStruct.comp ι₁₂ (horn 2 1).ι = stdSimplex.δ 0

The inclusion ι₁₂ : Δ[1] ⟶ Λ[2, 1] restricts Λ[2, 1].ι to the face map δ 0.

theorem SSet.horn₂₁.incl₂ : CategoryTheory.CategoryStruct.comp ι₀₁ (horn 2 1).ι = stdSimplex.δ 2

The inclusion ι₀₁ : Δ[1] ⟶ Λ[2, 1] restricts Λ[2, 1].ι to the face map δ 2.

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

noncomputable def SSet.horn₂₁.fromEdges {S : SSet} {x₀ x₁ x₂ : ((truncation 2).obj S).obj (Opposite.op { obj := { len := 0 }, property := ⋯ })} (e₀₁ : Edge x₀ x₁) (e₁₂ : 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₁₂ = SSet.horn₂₁.isPushout.desc (SSet.Truncated.Edge.edgeMap e₀₁) (SSet.Truncated.Edge.edgeMap e₁₂) ⋯

theorem SSet.horn₂₁.horn_from_edges_restr₀ {S : SSet} {x₀ x₁ x₂ : ((truncation 2).obj S).obj (Opposite.op { obj := { len := 0 }, property := ⋯ })} (e₀₁ : Edge x₀ x₁) (e₁₂ : 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 := { len := 0 }, property := ⋯ })} (e₀₁ : Edge x₀ x₁) (e₁₂ : 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 := { len := 0 }, property := ⋯ })} (e₀₁ : Edge x₀ x₁) (e₁₂ : Edge x₁ x₂) (g : stdSimplex.obj { len := 2 } ⟶ S) (comm : fromEdges e₀₁ e₁₂ = CategoryTheory.CategoryStruct.comp (horn 2 1).ι g) : (e₀₂ : 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.

theorem SSet.δ_comp_yonedaEquiv_symm_eq {S : SSet} {i j : Fin 3} {σ τ : S.obj (Opposite.op { len := 2 })} (h : (CategoryTheory.ConcreteCategory.hom (S.map (SimplexCategory.δ i).op)) σ = (CategoryTheory.ConcreteCategory.hom (S.map (SimplexCategory.δ j).op)) τ) : CategoryTheory.CategoryStruct.comp (stdSimplex.map (SimplexCategory.δ i)) (yonedaEquiv.symm σ) = CategoryTheory.CategoryStruct.comp (stdSimplex.map (SimplexCategory.δ j)) (yonedaEquiv.symm τ)

If two 2-simplices of S have equal i-th and j-th faces, then the corresponding face restrictions Δ[1] ⟶ S of their classifying maps Δ[2] ⟶ S agree.

theorem SSet.horn₃₁.incl₀ : CategoryTheory.CategoryStruct.comp ι₀ (horn 3 1).ι = stdSimplex.δ 0

The face inclusions ι₀/ι₂/ι₃ : Δ[2] ⟶ Λ[3, 1] restrict Λ[3, 1].ι to δ 0/2/3.

theorem SSet.horn₃₁.incl₂ : CategoryTheory.CategoryStruct.comp ι₂ (horn 3 1).ι = stdSimplex.δ 2

theorem SSet.horn₃₁.incl₃ : CategoryTheory.CategoryStruct.comp ι₃ (horn 3 1).ι = stdSimplex.δ 3

noncomputable def SSet.horn₃₁.fromFaces {S : SSet} {x₀ x₁ x₂ x₃ : ((truncation 2).obj S).obj (Opposite.op { obj := { len := 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₃ : Truncated.Edge.CompStruct e₀₁ e₁₂ e₀₂) (f₀ : Truncated.Edge.CompStruct e₁₂ e₂₃ e₁₃) (f₂ : Truncated.Edge.CompStruct e₀₁ e₁₃ e₀₃) : (horn 3 1).toSSet ⟶ S

Glue the three faces f₃, f₀, f₂ into a map Λ[3, 1].toSSet ⟶ S via the multicoequalizer presentation of the horn (horn₃₁.desc). The three hypotheses are the compatibilities of the faces along their shared edges e₁₂, e₁₃, e₀₁.

Equations

• SSet.horn₃₁.fromFaces f₃ f₀ f₂ = SSet.horn₃₁.desc (SSet.yonedaEquiv.symm f₀.simplex) (SSet.yonedaEquiv.symm f₂.simplex) (SSet.yonedaEquiv.symm f₃.simplex) ⋯ ⋯ ⋯

theorem SSet.horn₃₁.horn_extension_face₀ {S : SSet} {x₀ x₁ x₂ x₃ : ((truncation 2).obj S).obj (Opposite.op { obj := { len := 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₃ : Truncated.Edge.CompStruct e₀₁ e₁₂ e₀₂) (f₀ : Truncated.Edge.CompStruct e₁₂ e₂₃ e₁₃) (f₂ : Truncated.Edge.CompStruct e₀₁ e₁₃ e₀₃) {g : stdSimplex.obj { len := 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 := { len := 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₃ : Truncated.Edge.CompStruct e₀₁ e₁₂ e₀₂) (f₀ : Truncated.Edge.CompStruct e₁₂ e₂₃ e₁₃) (f₂ : Truncated.Edge.CompStruct e₀₁ e₁₃ e₀₃) {g : stdSimplex.obj { len := 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 := { len := 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₃ : Truncated.Edge.CompStruct e₀₁ e₁₂ e₀₂) (f₀ : Truncated.Edge.CompStruct e₁₂ e₂₃ e₁₃) (f₂ : Truncated.Edge.CompStruct e₀₁ e₁₃ e₀₃) {g : stdSimplex.obj { len := 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 := { len := 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₃ : Truncated.Edge.CompStruct e₀₁ e₁₂ e₀₂) (f₀ : Truncated.Edge.CompStruct e₁₂ e₂₃ e₁₃) (f₂ : Truncated.Edge.CompStruct e₀₁ e₁₃ e₀₃) (g : stdSimplex.obj { len := 3 } ⟶ S) (comm : fromFaces f₃ f₀ f₂ = CategoryTheory.CategoryStruct.comp (horn 3 1).ι g) : Truncated.Edge.CompStruct e₀₂ 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.

theorem SSet.horn₃₂.incl₀ : CategoryTheory.CategoryStruct.comp ι₀ (horn 3 2).ι = stdSimplex.δ 0

The face inclusions ι₀/ι₁/ι₃ : Δ[2] ⟶ Λ[3, 2] restrict Λ[3, 2].ι to δ 0/1/3.

theorem SSet.horn₃₂.incl₁ : CategoryTheory.CategoryStruct.comp ι₁ (horn 3 2).ι = stdSimplex.δ 1

theorem SSet.horn₃₂.incl₃ : CategoryTheory.CategoryStruct.comp ι₃ (horn 3 2).ι = stdSimplex.δ 3

noncomputable def SSet.horn₃₂.fromFaces {S : SSet} {x₀ x₁ x₂ x₃ : ((truncation 2).obj S).obj (Opposite.op { obj := { len := 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₃ : Truncated.Edge.CompStruct e₀₁ e₁₂ e₀₂) (f₀ : Truncated.Edge.CompStruct e₁₂ e₂₃ e₁₃) (f₁ : Truncated.Edge.CompStruct e₀₂ e₂₃ e₀₃) : (horn 3 2).toSSet ⟶ S

Glue the three faces f₃, f₀, f₁ into a map Λ[3, 2].toSSet ⟶ S via the multicoequalizer presentation of the horn (horn₃₂.desc). The three hypotheses are the compatibilities of the faces along their shared edges e₀₂, e₁₂, e₂₃.

Equations

• SSet.horn₃₂.fromFaces f₃ f₀ f₁ = SSet.horn₃₂.desc (SSet.yonedaEquiv.symm f₀.simplex) (SSet.yonedaEquiv.symm f₁.simplex) (SSet.yonedaEquiv.symm f₃.simplex) ⋯ ⋯ ⋯

theorem SSet.horn₃₂.horn_extension_face₀ {S : SSet} {x₀ x₁ x₂ x₃ : ((truncation 2).obj S).obj (Opposite.op { obj := { len := 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₃ : Truncated.Edge.CompStruct e₀₁ e₁₂ e₀₂) (f₀ : Truncated.Edge.CompStruct e₁₂ e₂₃ e₁₃) (f₁ : Truncated.Edge.CompStruct e₀₂ e₂₃ e₀₃) {g : stdSimplex.obj { len := 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 := { len := 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₃ : Truncated.Edge.CompStruct e₀₁ e₁₂ e₀₂) (f₀ : Truncated.Edge.CompStruct e₁₂ e₂₃ e₁₃) (f₁ : Truncated.Edge.CompStruct e₀₂ e₂₃ e₀₃) {g : stdSimplex.obj { len := 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 := { len := 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₃ : Truncated.Edge.CompStruct e₀₁ e₁₂ e₀₂) (f₀ : Truncated.Edge.CompStruct e₁₂ e₂₃ e₁₃) (f₁ : Truncated.Edge.CompStruct e₀₂ e₂₃ e₀₃) {g : stdSimplex.obj { len := 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 := { len := 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₃ : Truncated.Edge.CompStruct e₀₁ e₁₂ e₀₂) (f₀ : Truncated.Edge.CompStruct e₁₂ e₂₃ e₁₃) (f₁ : Truncated.Edge.CompStruct e₀₂ e₂₃ e₀₃) (g : stdSimplex.obj { len := 3 } ⟶ S) (comm : fromFaces f₃ f₀ f₁ = CategoryTheory.CategoryStruct.comp (horn 3 2).ι g) : Truncated.Edge.CompStruct e₀₁ 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.

@[implicit_reducible]

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

Left homotopy relation is reflexive

Equations

• ⋯ = ⋯

@[implicit_reducible]

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

Left homotopy relation is symmetric

Equations

• ⋯ = ⋯

@[implicit_reducible]

def SSet.Quasicategory₂.HomotopicL.trans {A : Truncated 2} [A.Quasicategory₂] {x y : A.obj (Opposite.op { obj := { len := 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

• ⋯ = ⋯

@[implicit_reducible]

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

Right homotopy relation is reflexive

Equations

• ⋯ = ⋯

@[implicit_reducible]

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

Right homotopy relation is symmetric

Equations

• ⋯ = ⋯

@[implicit_reducible]

def SSet.Quasicategory₂.HomotopicR.trans {A : Truncated 2} [A.Quasicategory₂] {x y : A.obj (Opposite.op { obj := { len := 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 := { len := 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 := { len := 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 := { len := 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 := { len := 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 := { len := 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 := { len := 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 := { len := 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')

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

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

Equations

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

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

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

• SSet.Quasicategory₂.quotientFunctor₂ = CategoryTheory.ReflQuiv.adj.homEquiv.invFun SSet.Quasicategory₂.quotientReflPrefunctor₂

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

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

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

theorem SSet.Quasicategory₂.composeEdges_unique {A : Truncated 2} [A.Quasicategory₂] {x₀ x₁ x₂ : A.obj (Opposite.op { obj := { len := 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 (f.comp 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₂.qFunctor_respects_horel₂ {A : Truncated 2} [A.Quasicategory₂] (x y : CategoryTheory.Cat.FreeRefl (OneTruncation₂ A)) (f g : x ⟶ y) (r : OneTruncation₂.HoRel₂ A 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 := { len := 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 = f

def SSet.Quasicategory₂.edgeToFreeHom {A : Truncated 2} {x₀ x₁ : A.obj (Opposite.op { obj := { len := 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.HomRel.CompClosure (CategoryTheory.Cat.FreeReflRel (SSet.OneTruncation₂ A))) (SSet.Quasicategory₂.edgeToHom f).toPath

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

theorem SSet.Quasicategory₂.homotopic_edges_are_equiv {A : Truncated 2} {x₀ x₁ : A.obj (Opposite.op { obj := { len := 0 }, property := ⋯ })} (f g : Truncated.Edge x₀ x₁) (htpy : Truncated.HomotopicL f g) : OneTruncation₂.HoRel₂ A (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 u_1} [CategoryTheory.ReflQuiver C] (F : CategoryTheory.Cat.FreeRefl (OneTruncation₂ A) ⥤rq C) (h : ∀ (x y : CategoryTheory.Cat.FreeRefl (OneTruncation₂ A)) (f g : x ⟶ y), OneTruncation₂.HoRel₂ A f g → F.map f = F.map g) : A.HomotopyCategory₂ ⥤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₂ : A.HomotopyCategory₂ ⥤rq C) (h : quotientReflPrefunctor₂ ⋙rq F₁ = quotientReflPrefunctor₂ ⋙rq F₂) : F₁ = F₂

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

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.