Paolo Giarrusso (May 13 2022 at 08:16): 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...
Karl Palmskog (May 13 2022 at 11:07):doesn't this have to do with the impredicative-set option?
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.
Abort.
Goal Set.
Succeed destruct absurd_prop.
Succeed destruct absurd.
Abort.
the system doesn't really expect you to type algebraic universes
Last updated: Oct 03 2023 at 04:02 UTC