(directed enhancement of homotopy type theory with types behaving like -categories)
Segal types are the (infinity,1)-categorical version of precategories in simplicial type theory
In simplicial type theory, a Segal type is a type such that given elements , , and and morphisms and , the type
is a contractible type, where is the -simplex probe shape and is its boundary.
Last revised on September 19, 2023 at 14:36:52. See the history of this page for a list of all contributions to it.