Update the HIT_README file for rewriting

[ruhatch]

HITs have changed to use the REWRITE rules for computation and have become much simpler, so I think the README should reflect this.

[favonia]

@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. :worried: Maybe others (or you?) can help?

[ruhatch]

@favonia Sadly I am also occupied right now, but I should be able to help in a few weeks' time

[gprop]

How would one define S1 using the new rewrite rules?

[favonia]

@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