Questions tagged [coq-unimath]

Use this tag when referencing the GitHub repository https://github.com/UniMath/UniMath.

Filter by
Sorted by
Tagged with
5 votes
0 answers
86 views

Prove equality in a record type

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

Found type UU where "?T" was expected

I am trying to solve a couple of exercises in coq. However, with the following code: ...
user avatar
4 votes
1 answer
154 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 ...
user avatar