Z-isSet.agda

{-# OPTIONS --cubical #-}
module _ where

open import Cubical.Foundations.Everything
open import Cubical.Data.Nat
open import Cubical.Data.Sum
open import Cubical.Data.Empty as ⊥
open import Cubical.Relation.Nullary

data ℤ : Type where
  diff : (x y : ℕ) → ℤ
  shift : ∀ x y → diff (suc x) (suc y) ≡ diff x y

to : ℤ → ℕ ⊎ ℕ
to (diff zero y) = inr y
to (diff (suc x) zero) = inl (suc x)
to (diff (suc x) (suc y)) = to (diff x y)
to (shift zero y i) = inr y
to (shift (suc x) zero i) = inl (suc x)
to (shift (suc x) (suc y) i) = to (diff x y)

from : ℕ ⊎ ℕ → ℤ
from (inl x) = diff x 0
from (inr y) = diff 0 y

ret : ∀ z → from (to z) ≡ z
ret (diff zero y) = refl
ret (diff (suc x) zero) = refl
ret (diff (suc x) (suc y)) = ret (diff x y) ∙ shift x y ⁻¹
ret (shift zero y i) = compPath-filler refl (shift 0 y ⁻¹) (~ i)
ret (shift (suc x) zero i) = compPath-filler refl (shift (suc x) 0 ⁻¹) (~ i)
ret (shift (suc x) (suc y) i) = compPath-filler (ret (diff x y) ∙ shift x y ⁻¹) (shift (suc x) (suc y) ⁻¹) (~ i)

-- This should be enough to conclude that ℤ is a set, as a retract of ℕ ⊎ ℕ which is a set.
-- Here's what I was initially trying to do:

inl≢inr : {A B : Type} {a : A} {b : B} → ¬ inl a ≡ inr b
inl≢inr p = subst (λ { (inl _) → Unit; (inr _) → ⊥}) p tt

diff-inj-0 : {x1 x2 : ℕ} → diff x1 0 ≡ diff x2 0 → x1 ≡ x2
diff-inj-0 {zero} {zero} p = refl
diff-inj-0 {zero} {suc x2} p = ⊥.rec (inl≢inr (cong to p ⁻¹))
diff-inj-0 {suc x1} {zero} p = ⊥.rec (inl≢inr (cong to p))
diff-inj-0 {suc x1} {suc x2} p = invEq (cong inl , isEmbedding-inl _ _) (cong to p)

diff-0-inj : {y1 y2 : ℕ} → diff 0 y1 ≡ diff 0 y2 → y1 ≡ y2
diff-0-inj {y1} {y2} p = invEq (cong inr , isEmbedding-inr _ _) (cong to p)

discrete-diff : (x1 y1 x2 y2 : ℕ) → Dec (diff x1 y1 ≡ diff x2 y2)
discrete-diff x1 0 x2 0 with discreteℕ x1 x2
... | yes x1≡x2 = yes (cong (λ x → diff x 0) x1≡x2)
... | no x1≢x2 = no λ p → x1≢x2 (diff-inj-0 p)
discrete-diff 0 y1 0 y2 with discreteℕ y1 y2
... | yes y1≡y2 = yes (cong (λ y → diff 0 y) y1≡y2)
... | no y1≢y2 = no λ p → y1≢y2 (diff-0-inj p)
discrete-diff 0 (suc y1) (suc x2) 0 = no λ p → inl≢inr (cong to p ⁻¹)
discrete-diff (suc x1) 0 0 (suc y2) = no λ p → inl≢inr (cong to p)
discrete-diff x1 y1 (suc x2) (suc y2) with discrete-diff x1 y1 x2 y2
... | yes p = yes (p ∙ shift x2 y2 ⁻¹)
... | no ¬p = no λ q → ¬p (q ∙ shift x2 y2)
discrete-diff (suc x1) (suc y1) x2 y2 with discrete-diff x1 y1 x2 y2
... | yes p = yes (shift x1 y1 ∙ p)
... | no ¬p = no λ q → ¬p (shift x1 y1 ⁻¹ ∙ q)

discreteℤ : Discrete ℤ
discreteℤ (diff x1 y1) (diff x2 y2) = discrete-diff x1 y1 x2 y2
discreteℤ (diff x1 y1) (shift x2 y2 i) = p i where
  p : PathP (λ i → Dec (diff x1 y1 ≡ shift x2 y2 i))
            (discrete-diff x1 y1 (suc x2) (suc y2))
            (discrete-diff x1 y1 x2 y2)
  p = {!   !}
discreteℤ (shift x1 y1 i) (diff x2 y2) = p i where
  p : PathP (λ i → Dec (shift x1 y1 i ≡ diff x2 y2))
            (discrete-diff (suc x1) (suc y1) x2 y2)
            (discrete-diff x1 y1 x2 y2)
  p = {!   !}
discreteℤ (shift x1 y1 i) (shift x2 y2 j) = {!   !}