Questions tagged [coq-unimath]
Use this tag when referencing the GitHub repository https://github.com/UniMath/UniMath.
5
questions
1
vote
0
answers
47
views
how to inductively define paths from paths using unimath
I'd like to define a type of graph where given a set of edges, we can define another graph that has everything from graph 1 but extends the set of edges by adding higher level edges to parallel edges(...
- 71
0
votes
0
answers
46
views
How to import unimath for coq
I want to be able to import the category theory module from unimath. I already have the coqide and vscode with the coq extensions, I also have wsl. I tried downloading the library from git and used &...
- 71
5
votes
0
answers
172
views
Prove equality in a record type
I am trying to prove something about monoids an categories. This results in the following (partial) proof:
...
- 265
3
votes
1
answer
104
views
Found type UU where "?T" was expected
I am trying to solve a couple of exercises in coq. However, with the following code:
...
- 265
5
votes
1
answer
327
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 ...
- 265