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

Showing changes from revision #1 to #2: Added | Removed | Changed

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:

TODO: Induction principle

References

• HoTT book