HoTT/HoTT-Agda

Update the HIT_README file for rewriting

ruhatch opened this issue · 4 comments

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

@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?

@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?

@gprop A direct definition would be something like

postulate
  : Type₀
  base :loop : base == base

module S¹Elim {l} {P : 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