Homotopy Type Theory empty type > history (Rev #2)


The empty type 0\mathbf{0} is the type with nothing in it. Or put differently, the type with no term constructors. This means we cannot make a term of the empty type.

The empty type is useful in logic since if a term can be constructed then you have run into a contradiction.

A proposition AA may be logically negated by writing A0A \to \mathbf{0}, since constructing such a term would mean AA cannot be true.

The empty type plays a similar role to the empty-set in set-theory. In fact in HoTT the empty set is the empty type.


The empty type exists:

0:𝒰\frac{}{\mathbf{0} : \mathcal{U}}

TODO: Induction principle


Revision on June 15, 2022 at 22:51:06 by Anonymous?. See the history of this page for a list of all contributions to it.