6
votes
Accepted
Cannot discriminate `0 = 1`
UniMath redefines the notation x = y away from Coq's standard eq (without also replacing ...
- 573
3
votes
Accepted
Found type UU where "?T" was expected
This is a universe inconsistency. You might get slightly more details with Set Printing Universes.. The type ∑ is defined in <...
- 1,547
Only top scored, non community-wiki answers of a minimum length are eligible