experiment with HITs and rewritng rules #2887
Annotations
1 error
|
Run coq-community/docker-coq-action@v1:
theories/PropResizing/ImpredicativeTruncation.v#L41
In environment
H : PropResizing
H0 : Funext
A : Type
f : typeofid A
The term "functor_merely f" has type "merely A -> merely A"
while it is expected to have type "typeofid (merely A)"
(universe inconsistency: Cannot enforce ap.u <=
HoTT.PropResizing.ImpredicativeTruncation.202 because
HoTT.PropResizing.ImpredicativeTruncation.202
< HoTT.PropResizing.ImpredicativeTruncation.204 <= ap.u).
Command exited with non-zero status 1
|
Loading