## Stream: new members

### Topic: Function between empty types

#### Sebastián Galkin (Aug 21 2020 at 21:36):

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 (Aug 21 2020 at 21:38):

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 (Aug 21 2020 at 21:38):

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

#### Adam Topaz (Aug 21 2020 at 21:39):

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

#### Sebastián Galkin (Aug 21 2020 at 21:41):

Brilliant, thank you.

#### Adam Topaz (Aug 21 2020 at 21:43):

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 (Aug 21 2020 at 21:43):

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

#### Sebastián Galkin (Aug 21 2020 at 21:44):

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

#### Adam Topaz (Aug 21 2020 at 21:45):

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 (Aug 21 2020 at 21:46):

Or something like that.

#### Sebastián Galkin (Aug 21 2020 at 21:47):

There is empty defined as an inductive type without constructors

#### Sebastián Galkin (Aug 21 2020 at 21:47):

But I was struggling with the \not nonempty construction

#### Adam Topaz (Aug 21 2020 at 21:51):

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

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


#### Adam Topaz (Aug 21 2020 at 21:56):

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 (Aug 21 2020 at 22:03):

Very nice, thank you.

Last updated: May 14 2021 at 04:22 UTC