Types that are empty #
In this file we define a typeclass IsEmpty
, which expresses that a type has no elements.
Main declaration #
IsEmpty
: a typeclass that expresses that a type is empty.
subtypes by false are false.
Non-dependent version of IsEmpty.elim
. Helpful if the elaborator cannot elaborate h.elim a
correctly.
Instances For
theorem
Function.extend_of_isEmpty
{α : Sort u_1}
{β : Sort u_2}
{γ : Sort u_3}
[IsEmpty α]
(f : α → β)
(g : α → γ)
(h : β → γ)
:
Function.extend f g h = h