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 23:24:38
by Urs Schreiber
(131.174.190.72)