Theorems · Inductive type · algebraic topology

SSet.Truncated.Edge

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

In a 2-truncated simplicial set, an edge from a vertex x₀ to x₁ is a 1-simplex with prescribed 0-dimensional faces.

Defined in

Mathlib.AlgebraicTopology.SimplicialSet.CompStructTruncated

Cited by

81 results in Mathlib

Foundations

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