Showing changes from revision #2 to #3:
Added | Removed | Changed
The empty type 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 may be logically negated by writing , since constructing such a term would mean 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:
TODO: Induction principle
Last revised on June 16, 2022 at 11:42:44. See the history of this page for a list of all contributions to it.