jespercockx/cubes
An implementation of (some fragment of) cubical type theory using rewrite rules, based on a talk given by Conor McBride at the 23rd Agda's Implementor's Meeting.
Agda
Issues
- 4
I = Squash Bool ?
#2 opened by andreasabel - 1
An implementation of (some fragment of) cubical type theory using rewrite rules, based on a talk given by Conor McBride at the 23rd Agda's Implementor's Meeting.
Agda