(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
Last revised on June 9, 2022 at 13:30:24. See the history of this page for a list of all contributions to it.