ZZ.agda

-- Thorsten Altenkirch demonstrates a bit of cubical agda preview in
-- his Lambda Days 2019 talk: Why Type Theory matters.
-- https://www.youtube.com/watch?v=DllYOFw5Qio
--
-- The slides don't reveal everything. It took me few attempts,
-- but  finally succeeded in filling-the-blanks quest.
-- It was a lot easier since agda/cubical library got more HIT examples.
--
{-# OPTIONS --cubical --safe #-}
module ZZ where

open import Cubical.Core.Everything

open import Cubical.Foundations.Prelude
open import Cubical.HITs.SetTruncation
open import Cubical.Foundations.HLevels
open import Cubical.HITs.SetTruncation
open import Cubical.Foundations.Isomorphism

open import Cubical.Data.Int
open import Cubical.Data.Nat

data ℤ : Set where
  zero : ℤ
  succ : ℤ → ℤ
  pred : ℤ → ℤ

  succpred : ∀ z → succ (pred z) ≡ z
  predsucc : ∀ z → pred (succ z) ≡ z

  trunc : isSet ℤ

module ZElim {ℓ} {B : ℤ → Type ℓ}
  (zero* : B zero)
  (succ* : {z : ℤ} → B z → B (succ z))
  (pred* : {z : ℤ} → B z → B (pred z))
  (succpred* : {z : ℤ} (b : B z) → PathP (λ i → B (succpred z i) ) (succ* (pred* b)) b)
  (predsucc* : {z : ℤ} (b : B z) → PathP (λ i → B (predsucc z i) ) (pred* (succ* b)) b)
  (trunc* : (z : ℤ) → isSet (B z))
  where

  f : (z : ℤ) → B z
  f zero                = zero*
  f (succ z)            = succ* (f z)
  f (pred z)            = pred* (f z)
  f (succpred z i)      = succpred* (f z) i
  f (predsucc z i)      = predsucc* (f z) i
  f (trunc n m p q i j) = elimSquash₀ trunc* (trunc n m p q) (f n) (f m) (cong f p) (cong f q) i j 

module ZElimProp {ℓ} {B : ℤ → Type ℓ} (BProp : {z : ℤ} → isProp (B z))
  (zero* : B zero)
  (succ* : {z : ℤ} → B z → B (succ z))
  (pred* : {z : ℤ} → B z → B (pred z))
  where

  f : (z : ℤ) → B z
  f = ZElim.f zero* succ* pred*
    (λ {z} b → toPathP (BProp (transp (λ i → B (succpred z i)) i0 (succ* (pred* b))) b))
    (λ {z} b → toPathP (BProp (transp (λ i → B (predsucc z i)) i0 (pred* (succ* b))) b))
    (λ z → isProp→isSet BProp)

module ZRec {ℓ} {B : Type ℓ} (BType : isSet B)
  (zero* : B)
  (succ* : B → B)
  (pred* : B → B)
  (succpred* : (b : B) → succ* (pred* b) ≡ b)
  (predsucc* : (b : B) → pred* (succ* b) ≡ b)
  where

  f : ℤ → B
  f = ZElim.f zero* succ* pred* succpred* predsucc* (λ _ → BType)

module Properties where
  ℤ-isSet : isSet ℤ
  ℤ-isSet = trunc

  ℤ→Int : ℤ → Int
  ℤ→Int = ZRec.f isSetInt (pos 0) sucInt predInt sucPred predSuc

  Int→ℤ : Int → ℤ
  Int→ℤ (pos n)    = iter n succ zero
  Int→ℤ (negsuc n) = iter n pred (pred zero)

  lem1 : ∀ n → ℤ→Int (iter n succ zero) ≡ pos n
  lem1 zero    = refl
  lem1 (suc n) = cong sucInt (lem1 n)

  lem2 : ∀ n → ℤ→Int (iter n pred (pred zero)) ≡ negsuc n
  lem2 zero    = refl
  lem2 (suc n) = cong predInt (lem2 n)

  Int→ℤ→Int : ∀ (z : Int) → ℤ→Int (Int→ℤ z) ≡ z
  Int→ℤ→Int (pos n)    = lem1 n
  Int→ℤ→Int (negsuc n) = lem2 n

  lem3 : ∀ z → Int→ℤ (sucInt z) ≡ succ (Int→ℤ z)
  lem3 (pos n) = refl
  lem3 (negsuc zero) = sym (succpred zero)
  lem3 (negsuc (suc n)) = sym (succpred _)

  lem4 : ∀ z →  Int→ℤ (predInt z) ≡ pred (Int→ℤ z)
  lem4 (pos zero)    = refl
  lem4 (pos (suc n)) = sym (predsucc _)
  lem4 (negsuc n)    = refl

  ℤ→Int→ℤ : ∀ (z : ℤ) → Int→ℤ (ℤ→Int z) ≡ z
  ℤ→Int→ℤ = ZElimProp.f {B = λ z → Int→ℤ (ℤ→Int z) ≡ z} (ℤ-isSet _ _)
    refl
    (λ {z} p → lem3 (ℤ→Int z) ∙ cong succ p)
    (λ {z} p → lem4 (ℤ→Int z) ∙ cong pred p)

  Int≡ℤ : Int ≡ ℤ
  Int≡ℤ = isoToPath (iso Int→ℤ ℤ→Int ℤ→Int→ℤ Int→ℤ→Int)

-- Examples
module Ex where
  open import Cubical.Data.Bool
  open import Cubical.Relation.Nullary
  open import Cubical.Relation.Nullary.DecidableEq

  -- We know that Int is discrete (i.e. has decidable equality)
  -- so ℤ is discrete as well!
  discreteℤ : Discrete ℤ
  discreteℤ = subst Discrete Properties.Int≡ℤ discreteInt

  -- let's try to compute!
  -- I strip to Bool as otherwise Agda takes ages to compute the evidence
  ex₁ : Dec→Bool (discreteℤ (pred (succ zero)) (succ (pred zero))) ≡ true
  ex₁ = refl

  ex₂ : Dec→Bool (discreteℤ (pred (succ zero)) (succ (pred (pred zero)))) ≡ false
  ex₂ = refl