Zulip Chat Archive

Stream: new members

Topic: Function between empty types


view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip Adam Topaz (Aug 21 2020 at 21:38):

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

view this post on Zulip 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.

view this post on Zulip Sebastián Galkin (Aug 21 2020 at 21:41):

Brilliant, thank you.

view this post on Zulip 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.

view this post on Zulip Adam Topaz (Aug 21 2020 at 21:43):

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

view this post on Zulip Sebastián Galkin (Aug 21 2020 at 21:44):

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

view this post on Zulip 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.

view this post on Zulip Adam Topaz (Aug 21 2020 at 21:46):

Or something like that.

view this post on Zulip Sebastián Galkin (Aug 21 2020 at 21:47):

There is empty defined as an inductive type without constructors

view this post on Zulip Sebastián Galkin (Aug 21 2020 at 21:47):

But I was struggling with the \not nonempty construction

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Sebastián Galkin (Aug 21 2020 at 22:03):

Very nice, thank you.


Last updated: May 14 2021 at 04:22 UTC