qiitInt

-- 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)
def neg : El I → El I ≔
  λi. IElim (λw. I) zero (λx. λih. pred ih) (λx. λih. suc ih)
        (λx. λih. ⋆) (λx. λih. ⋆) i

def negSucPred : neg (suc (pred zero)) ≡ zero ∈ _ ≔ ⋆
def negPred : neg (pred zero) ≡ suc zero ∈ _ ≔ ⋆