Background
Basic concepts
equivalences in/of -categories
Universal constructions
Local presentation
Theorems
Extra stuff, structure, properties
Models
A simplicial -groupoid or simplicial anima is an (∞,1)-functor
from the opposite category of the simplex category into the (∞,1)-category ∞Grpd of ∞-groupoids.
A -precategory is a simplicial infinity-groupoid which satisfies the Segal conditions;
A -category is a -precategory which also satisfies the univalence axiom;
An -groupoid or discrete -category is a -category all of whose morphisms are equivalences under composition.
The -category of simplicial -groupoids and morphisms between them is the (∞,1)-category of (∞,1)-functors
is the classifying -topos for linear intervals.
There is an inclusion
of -groupoids and of -categories inside . Furthermore, the Sierpinski -topos embeds into
There is also an automorphic -functor
on which takes a simplicial -groupoid to its opposite simplicial -groupoid. When restricted to the -subcategory , the -functor takes -categories to its opposite -category.
The simplicial interval (regarded under (∞,1)-Yoneda embedding) is a tiny object: there is an amazing right adjoint
on .
Since is an (∞,1)-topos, is a cohesive (∞,1)-topos over :
Here
sends a simplicial -groupoid to the homotopy colimit over its components, hence to its “geometric realization” as seen in .
evaluates on the 0-simplex;
sends a simplicial -groupoid to the simplicial object which is simplicially constant on .
Hence cohesion of relative to expresses the existence of a discrete and directed notion of path.
The simplicial interval (regarded under (∞,1)-Yoneda embedding) exhibits the cohesion of over , in that the relative shape modality is equivalent to the localization at
The -category of simplicial -groupoids is the internal logic is given by simplicial type theory, a cohesive modal homotopy type theory equipped with the axioms for a linear interval and an axiom of cohesion for the linear interval.
Simplicial -groupoids can be modeled by bisimplicial sets.
Last revised on April 12, 2025 at 12:15:36. See the history of this page for a list of all contributions to it.