agda / cubical

An experimental library for Cubical Agda
https://agda.github.io/cubical/Cubical.README.html
Other
441 stars 134 forks source link

Construct 'the' free wild category on a graph #1117

Closed felixwellen closed 2 months ago

felixwellen commented 3 months ago

This is part of an experiment to see if there is an easy-to-have solver for wild categories. I don't know if that will actually just work and I don't know if what I construct here can actually be called the free wild category. This depends PR on #1116