(in category theory/type theory/computer science)
of all homotopy types
of (-1)-truncated types/h-propositions
natural deduction metalanguage, practical foundations
type theory (dependent, intensional, observational type theory, homotopy type theory)
computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory
A reflective sub-universe. If closed under dependent sum, then this is the universe of modal types for a modal operator.
For the relation to modal type theory see Rijke, Shulman, Spitters.
…in categorical semantics this means that it is an exponential ideal, hence that the reflector preserves finite products
Univalent Foundations Project, section 7.7 of Homotopy Type Theory – Univalent Foundations of Mathematics
Egbert Rijke, Mike Shulman, Bas Spitters, Modalities in homotopy type theory arXiv
Last revised on June 28, 2017 at 04:40:43. See the history of this page for a list of all contributions to it.