## Idea The empty type $\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]] $A$ may be logically negated by writing $A \to \mathbf{0}$, since constructing such a term would mean $A$ 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. ## Definition The empty type exists: $$\frac{}{\mathbf{0} : \mathcal{U}}$$ TODO: Induction principle ## References * [[HoTT book]] category: not redirected to nlab yet