Upgrade identity systems

cmcmA20 / cubical-mini

GNU Affero General Public License v3.0

6 stars 7 forks source link

Open cmcmA20 opened 5 months ago

cmcmA20 commented 5 months ago

[ ] Displayed identity systems, preferably with an explicit characterization of transport
[ ] Dependent version of Extensional class
[x] Common equational reasoning syntax
[ ] Composition operator and groupoid laws parameterized by an identity system

cmcmA20 commented 5 months ago

I suppose implementing #32 would be much cleaner after this