Update the HIT_README file for rewriting
ruhatch opened this issue · 4 comments
ruhatch commented
HITs have changed to use the REWRITE rules for computation and have become much simpler, so I think the README should reflect this.
favonia commented
@ruhatch Thanks for bringing this up! I added some note in the file to clarify. Unfortunately right now I am too occupied to make a complete rewrite. 😟 Maybe others (or you?) can help?
ruhatch commented
@favonia Sadly I am also occupied right now, but I should be able to help in a few weeks' time
gprop commented
How would one define S1 using the new rewrite rules?
favonia commented
@gprop A direct definition would be something like
postulate
S¹ : Type₀
base : S¹
loop : base == base
module S¹Elim {l} {P : S¹ → Type l}
(base* : P base) (loop* : base* == base* [ P ↓ loop ]) where
postulate
f : Π S¹ P
base-β : f base ↦ base*
{-# REWRITE base-β #-}
postulate
loop-β : apd f loop == loop*
S¹-elim = S¹Elim.f