Function between empty types

Stream: new members

[Sebastián Galkin]

How to remove sorry in this

variables A B: Type*
variable ha: ¬ nonempty (unit → A)
variable hb: ¬ nonempty (unit → B)

example  : A → B := sorry

[Adam Topaz]

variables A B: Type*
variable ha: ¬ nonempty (unit → A)
variable hb: ¬ nonempty (unit → B)

include ha
example  : A → B := λ a, false.elim (ha ⟨λ _, a⟩)

[Adam Topaz]

In general, false.elim is a way to produce anything from a proof of false.

[Adam Topaz]

And given a : A, together with your ha, you can produce a proof of false as in the above code.

[Sebastián Galkin]

Brilliant, thank you.

[Adam Topaz]

One thing to note: You need to include the include ha for otherwise it would not be in the context of the example.

[Adam Topaz]

And you don't really need hb, at least for this example.

[Sebastián Galkin]

Makes sense, you can always produce the function from the empty type to anything

[Adam Topaz]

There was some discussion a while back about making a standard definition for "this is an empty type", did that ever converge? If I recall correctly the leading contender was def is_empty (A : Type*) := A \to false.

[Adam Topaz]

Or something like that.

[Sebastián Galkin]

There is empty defined as an inductive type without constructors

[Sebastián Galkin]

But I was struggling with the \not nonempty construction

[Adam Topaz]

variables A B: Type*
variable h: A → false

include h
example : A → B := λ a, false.elim $ h a

[Adam Topaz]

And in case you actually need the "not nonempty" version:

example {A : Type*} : ¬(nonempty A) ↔ (A → false) := ⟨λ h a, h ⟨a⟩, λ f ⟨a⟩, f a⟩

[Sebastián Galkin]

Very nice, thank you.