agda / cubical

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

Refactor and extend the path-graph #1116

Closed felixwellen closed 2 months ago

felixwellen commented 3 months ago

The path graph consists of the inductive type of composable lists of edges. now the constructors have the same argument order as lists and everything is phrased in diagrammatic order. Some coherences have been added and a 'map' for path-graphs.