Mathlib Map

Structures · Topology

SSet.IsStrictSegal

For X a simplicial set, IsStrictSegal X asserts the mere existence of an inverse to spine X n for all n : ℕ.

Defined in
Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
Shape
One type argument · adds segal

Extends0

Extends nothing: this is a root of the hierarchy.

Extended by0

Nothing extends this class yet.

Forgetful instances

Every SSet.IsStrictSegal is also a

Concrete types that are instances1

  • CategoryTheory.nerve

How is a type an instance?

Loading the hierarchy index…

Assumed by5

Ancestors1