HoTT-categories
HoTT-categories copied to clipboard
CategoricalData
A category theory library built on top of Homotopy Type Theory, by Jason Gross
The objects in a path category are paths of edges in a graph. https://bitbucket.org/JasonGross/catdb/src/4eb6407c6ca3200bebefaa3a1834d05c49b01846/PathsCategory.v?at=default https://bitbucket.org/JasonGross/catdb/src/4eb6407c6ca3200bebefaa3a1834d05c49b01846/PathsCategoryFunctors.v?at=default
https://bitbucket.org/JasonGross/catdb/src/4eb6407c6ca3200bebefaa3a1834d05c49b01846/ChainCategory.v?at=default This requires proving that `le` `IsHProp`.
This is https://bitbucket.org/JasonGross/catdb/src/4eb6407c6ca3200bebefaa3a1834d05c49b01846/LtacReifiedSimplification.v?at=default https://bitbucket.org/JasonGross/catdb/src/4eb6407c6ca3200bebefaa3a1834d05c49b01846/TypeclassSimplification.v?at=default https://bitbucket.org/JasonGross/catdb/src/4eb6407c6ca3200bebefaa3a1834d05c49b01846/TypeclassUnreifiedSimplification.v?at=default https://bitbucket.org/JasonGross/catdb/src/4eb6407c6ca3200bebefaa3a1834d05c49b01846/CanonicalStructureSimplification.v?at=default
Metadata
Owner
Metadata
A category theory library built on top of Homotopy Type Theory, by Jason Gross