Towards Proof-Irrelevant Equality
I’m following a plan to get us to stage 2 of the equality story: proof irrelevance. I’ll update this post as I go, but so far I’ve
- split Term into syntactic stuff (still Term) and semantic stuff (new file Value)
- lumped the contents of Equality into Value and removed Equality
- threaded a freshroot through eval and everything which calls it (no fun at all)
- added source and target to coe and coh
- made the computational behaviour of coe and coh compare source with target if the proof isn’t already refl
- made normal proofs of equations equal
- made spine comparison of coe just compare sources and targets, rather than (irrelevant) proofs
- did some very basic testing
- pushed the changes
- gone in search of a drink
I’m trying to keep Epitome sane as I go.