nLab type of n-types

Context

Universes

$\vdash \sum_{X : Type} isNTruncated(X) : Type$
Created on September 11, 2012 23:24:38 by Urs Schreiber (131.174.190.72)