Background
Basic concepts
equivalences in/of -categories
Universal constructions
Local presentation
Theorems
Extra stuff, structure, properties
Models
category object in an (∞,1)-category, groupoid object
(directed enhancement of homotopy type theory with types behaving like -categories)
This entry is meant to be about the analog of the notion of gaunt categories for types of simplicial type theory.
The following definition is lacking reference or justification.
In simplicial type theory, a type is a gaunt type or stiff type if it is both a skeletal type and a univalent type.
If is also a Segal type, then the notion corresponds to the concept of a gaunt (infinity,1)-category.
Last revised on April 13, 2025 at 05:29:48. See the history of this page for a list of all contributions to it.