Timeline for Found type UU where "?T" was expected
Current License: CC BY-SA 4.0
13 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Apr 22, 2022 at 15:33 | comment | added | Andrej Bauer | Benedikt lives dangerously, with universe checking turned off... | |
| Apr 22, 2022 at 12:21 | vote | accept | Tempestas Ludi | ||
| Apr 22, 2022 at 12:21 | comment | added | Tempestas Ludi | @JasonGross Thank you for the explanation. I believe I now understand what is happening here and why it goes wrong. | |
| Apr 22, 2022 at 12:20 | comment | added | Tempestas Ludi | @AndrejBauer According to github.com/UniMath/Schools/blob/master/2019-04-Birmingham/…, it was Benedikt. I might ask him myself :-) | |
| Apr 22, 2022 at 7:24 | comment | added | Andrej Bauer | Who formulated the theorem, someone giving you the exercise or you yourself? It seems like the statement of the exercise is suboptimal. | |
| Apr 21, 2022 at 18:34 | comment | added | Jason Gross |
I've updated my answer; I didn't want to bother compiling UniMath and was assuming that the error was on exact. If you want to solve the problem without universe inconsistencies, you'll need to redefine all the types you want to sigma up from scratch as living in a smaller universe than UU. The reason UU and Type behave differently is because Coq has typical ambiguity and each use of Type is given its own universe. If UU were made universe-polymorphic, the same feature would apply to UU.
|
|
| Apr 21, 2022 at 18:32 | history | edited | Jason Gross | CC BY-SA 4.0 |
Explain actual universe error at the theorem statement rather than the exact
|
| Apr 21, 2022 at 12:00 | comment | added | Tempestas Ludi |
Also, the file UniMath.Foundations.Preamble has on one of the first lines Definition UU := Type. So why is there different behaviour when using UU vs Type?
|
|
| Apr 21, 2022 at 8:24 | comment | added | Tempestas Ludi | So would there be a way to solve this without allowing universe inconsistencies (because those would allow for paradoxes)? | |
| Apr 21, 2022 at 8:23 | comment | added | Tempestas Ludi |
Note that the first error is thrown at the line Theorem exercise_1_4: .... This does not yet have anything to do with the universe of fill_me, and indeed, is not solved by having fill_me work on a bigger universe. Also note that in UniMath, UU is defined as UU := Type.
|
|
| Apr 21, 2022 at 8:21 | comment | added | Tempestas Ludi |
Unset Universe Checking indeed solves my problem when I replace UU by Type.
|
|
| Apr 21, 2022 at 8:18 | comment | added | Tempestas Ludi |
Set Printing Universes does not yield any more information.
|
|
| Apr 20, 2022 at 14:39 | history | answered | Jason Gross | CC BY-SA 4.0 |