(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
In type theory the type of propositions corresponds roughly under categorical semantics to the subobject classifier. (To be precise, depending on the type theoretic rules and axioms this may not be quite true: one needs propositional resizing, propositional extensionality, and — in some type theories where “proposition” is not defined as an h-proposition, such as the calculus of constructions — the principle of unique choice?.)
Its generalization from propositions to general types is the type of types.
Detailed discussion of the type of propositions in Coq is in
Last revised on December 1, 2016 at 12:39:59. See the history of this page for a list of all contributions to it.