type of n-types

(in category theory/type theory/computer science)

**of all homotopy types**

**of (-1)-truncated types/h-propositions**

$\vdash \sum_{X : Type} isNTruncated(X) : Type$

Created on September 11, 2012 at 23:24:17. See the history of this page for a list of all contributions to it.