Questions tagged [coq-unimath]
Use this tag when referencing the GitHub repository https://github.com/UniMath/UniMath.
3
questions with no upvoted or accepted answers
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
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