Theorems · Inductive type · algebraic topology

SSet.Truncated.Edge.CompStruct

{X : SSet.Truncated 2} →
  {x₀ x₁ x₂ : X.obj (Opposite.op { obj := { len := 0 }, property := SSet.Truncated.Edge._proof_1 })} →
    SSet.Truncated.Edge x₀ x₁ → SSet.Truncated.Edge x₁ x₂ → SSet.Truncated.Edge x₀ x₂ → Type u

Let x₀, x₁, x₂ be 0-simplices of a 2-truncated simplicial set X, e₀₁ an edge from x₀ to x₁, e₁₂ an edge from x₁ to x₂, e₀₂ an edge from x₀ to x₂. This is the data of a 2-simplex whose faces are respectively e₀₂, e₁₂ and e₀₁. Such structures shall provide relations in the homotopy category of arbitrary (truncated) simplicial sets (and specialized constructions for quasicategories and Kan complexes.).

Defined in

Mathlib.AlgebraicTopology.SimplicialSet.CompStructTruncated

Cited by

28 results in Mathlib

Foundations

Depth 34 from the axioms · uses propext, Quot.sound