More flexible WildCat.Paths instances

HoTT / Coq-HoTT

A Coq library for Homotopy Type Theory

http://homotopytypetheory.org/

Other

1.25k stars 193 forks source link

Closed Alizter closed 3 months ago

Alizter commented 3 months ago

This allows wildcat structures to be augmented with paths in the higher cells.

cc @ThomatoTomato

jdchristensen commented 3 months ago

Ok, this LGTM! @ThomatoTomato this should help with the matrix category.