Towards Observational Equality
Thursday, January 26th, 2006OK, I think I have a plan. I’m gonna
- hack in Bool and W directly, leaving ‘data’ alone for the moment
- add the relevant extra eliminators for equations (dom, cod, sym)
- make coe go into functions, pairs and trees
- add a constructor for extensionality
If that works out, it’s time to rethink data, then remove Bool and W. I’ll keep youse posted.