Skip to main content

Questions tagged [coq-unimath]

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

Filter by
Sorted by
Tagged with
1 vote
0 answers
44 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(...
noCrayCray's user avatar
0 votes
0 answers
42 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 &...
noCrayCray's user avatar
5 votes
0 answers
156 views

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
96 views

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
5 votes
1 answer
292 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 ...
Tempestas Ludi's user avatar