Stream: Coq users

Topic: `False : Prop` vs `Empty_set : Set`

view this post on Zulip Paolo Giarrusso (May 13 2022 at 08:16):

I feel like I forgot about Empty_set (if I knew) and abused Prop a few times. This is probably confusing for readers (it was for me), but is it also buggy? Is there any reasoning principle that holds for one but not the other? Since False <-> Empty_set (right?) it seems hard to imagine...

view this post on Zulip Karl Palmskog (May 13 2022 at 11:07):

doesn't this have to do with the impredicative-set option?

view this post on Zulip Ali Caglayan (May 13 2022 at 11:15):

In the HoTT library we don't use Prop but have Empty which is just Empty_set and lives in Set. So far all the contradiction style tactics seem to work with that just fine, I am not aware of any special treatment. (By which I mean they are treated exactly the same).

Here is an example to show that you can eliminate from a Prop to a Set no problem if that Prop is False. So they end up acting the same. I also found some bonus anomalies when trying to eliminate to higher universes. (But that seems to be a missing case rather than anything serious. Type on its own works fine).

Axiom absurd_prop : False.
Axiom absurd : Empty_set.

Goal Type@{Set+1}.
Fail destruct absurd_prop.
Fail destruct absurd.

Goal Set.
Succeed destruct absurd_prop.
Succeed destruct absurd.

view this post on Zulip Gaëtan Gilbert (May 13 2022 at 11:49):

the system doesn't really expect you to type algebraic universes

Last updated: May 18 2024 at 10:02 UTC