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 simplicial skeleta and simplicial coskeleta for types of simplicial type theory.
1-coskeletal types are defined in section 9 of:
Last revised on June 8, 2025 at 17:37:08. See the history of this page for a list of all contributions to it.