type of propositions

(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* is what in the categorical semantics becomes the subobject classifier.

Its generalization from propositions to general types is the type of types in homotopy type theory.

Detailed discussion of the type of propositions in Coq is in

Revised on October 3, 2012 02:01:13
by Urs Schreiber
(82.169.65.155)