Questions tagged [coq-unimath]
Use this tag when referencing the GitHub repository https://github.com/UniMath/UniMath.
3
questions
5
votes
0
answers
115
views
Prove equality in a record type
I am trying to prove something about monoids an categories. This results in the following (partial) proof:
...
- 225
3
votes
1
answer
76
views
Found type UU where "?T" was expected
I am trying to solve a couple of exercises in coq. However, with the following code:
...
- 225
4
votes
1
answer
200
views
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 ...
- 225