Zulip Chat Archive

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: Dec 20 2023 at 11:08 UTC