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...

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

option?

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: Jan 29 2023 at 06:02 UTC