{-# OPTIONS --cubical #-}

open import Cubical.Foundations.Everything -- _∙_ is defined
open import Cubical.Data.Nat hiding (zero; _+_; +-comm; +-assoc)
open import Cubical.Data.Int

postulate
  magic : ∀ {ℓ} {X : Type ℓ} → X

infixl 5 _⊖_
data ΔInt : Type₀ where
  _⊖_    : ℕ → ℕ → ΔInt
  cancel : ∀ a b → a ⊖ b ≡ suc a ⊖ suc b

succ : ΔInt → ΔInt
succ (a ⊖ b) = suc a ⊖ b
succ (cancel a b i) = cancel (suc a) b i

pred : ΔInt → ΔInt
pred (a ⊖ b) = a ⊖ suc b
pred (cancel a b i) = cancel a (suc b) i

fromInt : Int → ΔInt
fromInt (pos n) = n ⊖ 0
fromInt (negsuc n) = 0 ⊖ suc n

{-
  _ℕ-_ : ℕ → ℕ → Int
  a ℕ- 0 = pos a
  0 ℕ- suc b = negsuc b
  suc a ℕ- suc b = a ℕ- b
-}
toInt : ΔInt → Int
toInt (a ⊖ b) = a ℕ- b
toInt (cancel a b i) = a ℕ- b

toInt-fromInt : ∀ n → toInt (fromInt n) ≡ n
toInt-fromInt (pos _) = refl
toInt-fromInt (negsuc _) = refl

diamond : ∀ {ℓ} {A : Type ℓ} {x y z : A} (p : x ≡ y) (q : y ≡ z) → (λ i → p i ≡ q i) [ p ≡ q ]
diamond {y = y} p q i j =
  hcomp
    (λ k → λ
      { (i = i0) → p (j ∨ ~ k)
      ; (i = i1) → q (j ∧ k)
      ; (j = i0) → p (i ∨ ~ k)
      ; (j = i1) → q (i ∧ k)
      }) y

triangle : ∀ {ℓ} {A : Type ℓ} {x y : A} (p : x ≡ y) → (λ i → x ≡ p i) [ refl ≡ refl ∙ p ]
triangle {x = x} p i j = hcomp (λ k → λ { (i = i0) → x; (j = i0) → x; (j = i1) → p (i ∧ k)}) x

-- This is very difficult.
fromInt-toInt : ∀ n → fromInt (toInt n) ≡ n
fromInt-toInt (a ⊖ 0) = refl
fromInt-toInt (0 ⊖ suc b) = refl
fromInt-toInt (suc a ⊖ suc b) = fromInt-toInt (a ⊖ b) ∙ cancel a b
fromInt-toInt (cancel a 0 i) = triangle (cancel a 0) i
fromInt-toInt (cancel 0 (suc b) i) = triangle (cancel 0 (suc b)) i
fromInt-toInt (cancel (suc a) (suc b) i) =
  fromInt-toInt (cancel a b i) ∙ diamond (cancel a b) (cancel (suc a) (suc b)) i

{- Part 2 -}

equiv : ∀ {ℓ₁ ℓ₂ : Level} {A : Type ℓ₁} {B : Type ℓ₂} (f : A → B) (g : B → A) (f-g : (y : B) → f (g y) ≡ y) (g-f : (x : A) → g (f x) ≡ x) → A ≃ B
equiv f g f-g g-f = isoToEquiv (iso f g f-g g-f)

Int≡ΔInt : Int ≡ ΔInt
Int≡ΔInt = ua (equiv fromInt toInt fromInt-toInt toInt-fromInt)

{-
  _+_ : Int → Int → Int
  m + pos n = m +pos n
  m + negsuc n = m +negsuc n
-}
_Δ+_ : ΔInt → ΔInt → ΔInt
_Δ+_ = transport (λ i → Int≡ΔInt i → Int≡ΔInt i → Int≡ΔInt i) _+_

+≡Δ+ : (λ i → Int≡ΔInt i → Int≡ΔInt i → Int≡ΔInt i) [ _+_ ≡ _Δ+_ ]
+≡Δ+ = transport-filler (λ i → Int≡ΔInt i → Int≡ΔInt i → Int≡ΔInt i) _+_

{- Hints: There are already many theorems about _+_. -}
{- Check out https://github.com/agda/cubical/blob/master/Cubical/Data/Int/Properties.agda -}
Δ+-comm : ∀ x y → x Δ+ y ≡ y Δ+ x
Δ+-comm = transport (λ i → ∀ (x y : Int≡ΔInt i) → +≡Δ+ i x y ≡ +≡Δ+ i y x) +-comm

Δ+-assoc : ∀ x y z → x Δ+ (y Δ+ z) ≡ (x Δ+ y) Δ+ z
Δ+-assoc = transport (λ i → ∀ (x y z : Int≡ΔInt i) → +≡Δ+ i x (+≡Δ+ i y z) ≡ +≡Δ+ i (+≡Δ+ i x y) z) +-assoc