Questions tagged [coq-unimath]

Use this tag when referencing the GitHub repository

Filter by
Sorted by
Tagged with
5 votes
0 answers

Prove equality in a record type

I am trying to prove something about monoids an categories. This results in the following (partial) proof: ...
Tempestas Ludi's user avatar
3 votes
1 answer

Found type UU where "?T" was expected

I am trying to solve a couple of exercises in coq. However, with the following code: ...
Tempestas Ludi's user avatar
4 votes
1 answer

Cannot discriminate `0 = 1`

I am just practicing a bit with coq, doing some UniMath exercises and am trying to prove (0 = 1) -> empty. However, for some reason, I seem unable to reason ...
Tempestas Ludi's user avatar