Qiit.int

-- Integers as a QIIT with RECURSIVE EQUALITY CONSTRAINTS: suc/pred
-- are mutually inverse, imposed as equations with INDUCTIVE binders.

data
  I : U
  zero : El I
  suc : El I → El I
  pred : El I → El I
  sucpred : (i : El I) → suc (pred i) ≡ i ∈ El I
  predsuc : (i : El I) → pred (suc i) ≡ i ∈ El I

-- negation by elimination: the coherences are the OTHER equation each
-- time (⟦suc (pred i)⟧ β-reduces to pred (suc ih), closed by predsuc)
neg : I → I using (predsuc, Qiit.int.I.unfold, Qiit.int.pred.eq, Qiit.int.suc.eq, sucpred)
neg = λi. IElim (λw. I) zero (λx ih. pred ih) (λx ih. suc ih) (λx ih. ⋆) (λx ih. ⋆) i

negSucPred : neg (suc (pred zero)) ≡ zero
  using (predsuc,
    Qiit.int.I.eq,
    Qiit.int.IElim.eq,
    Qiit.int.neg.eq,
    Qiit.int.pred.eq,
    Qiit.int.suc.eq,
    Qiit.int.zero.eq)
negSucPred = ⋆

negPred : neg (pred zero) ≡ suc zero
  using (Qiit.int.I.eq,
    Qiit.int.IElim.eq,
    Qiit.int.neg.eq,
    Qiit.int.pred.eq,
    Qiit.int.suc.eq,
    Qiit.int.zero.eq)
negPred = ⋆