{-# OPTIONS --without-K --exact-split #-}
open import TransportLemmas
open import EquivalenceType

open import HomotopyType
open import FunExtAxiom
open import QuasiinverseType
open import DecidableEquality
open import NaturalType
open import HLevelTypes
open import HedbergLemmas

Integers

module IntegerType where

  data: Type₀ where
    zer :pos :neg :-- Inclusion of the natural numbers into the integers
  NtoZ : ℤ
  NtoZ zero     = zer
  NtoZ (succ n) = pos n

  -- Successor function
  zsucc : ℤ
  zsucc zer            = pos 0
  zsucc (pos x)        = pos (succ x)
  zsucc (neg zero)     = zer
  zsucc (neg (succ x)) = neg x

  -- Predecessor function
  zpred : ℤ
  zpred zer            = neg 0
  zpred (pos zero)     = zer
  zpred (pos (succ x)) = pos x
  zpred (neg x)        = neg (succ x)

  -- Successor and predecessor
  zsuccpred-id : (n :)  zsucc (zpred n) == n
  zsuccpred-id zer            = refl _
  zsuccpred-id (pos zero)     = refl _
  zsuccpred-id (pos (succ n)) = refl _
  zsuccpred-id (neg n)        = refl _

  zpredsucc-id : (n :)  zpred (zsucc n) == n
  zpredsucc-id zer            = refl _
  zpredsucc-id (pos n)        = refl _
  zpredsucc-id (neg zero)     = refl _
  zpredsucc-id (neg (succ n)) = refl _

  zpredsucc-succpred : (n :)  zpred (zsucc n) == zsucc (zpred n)
  zpredsucc-succpred zer = refl zer
  zpredsucc-succpred (pos zero) = refl (pos zero)
  zpredsucc-succpred (pos (succ x)) = refl (pos (succ x))
  zpredsucc-succpred (neg zero) = refl (neg zero)
  zpredsucc-succpred (neg (succ x)) = refl (neg (succ x))

  zsuccpred-predsucc : (n :)  zsucc (zpred n) == zpred (zsucc n)
  zsuccpred-predsucc n = inv (zpredsucc-succpred n)

  -- Equivalence given by successor and predecessor
  zequiv-succ : ℤ ≃ ℤ
  zequiv-succ = qinv-≃ zsucc (zpred , (zsuccpred-id , zpredsucc-id))

  -- Negation
  private
    - : ℤ
    - zer     = zer
    - (pos x) = neg x
    - (neg x) = pos x

  double- : (z :)  - (- z) == z
  double- zer = refl _
  double- (pos x) = refl _
  double- (neg x) = refl _

  zequiv- : ℤ ≃ ℤ
  zequiv- = qinv-≃ - (- , (double- , double-))

  -- Addition on integers
  infixl 60 _+ᶻ_
  _+ᶻ_ : ℤ
  zer +ᶻ m = m
  pos zero +ᶻ m = zsucc m
  pos (succ x) +ᶻ m = zsucc (pos x +ᶻ m)
  neg zero +ᶻ m = zpred m
  neg (succ x) +ᶻ m = zpred (neg x +ᶻ m)

  -- s on addition
  +ᶻ-lunit : (n :)  n == n +ᶻ zer
  +ᶻ-lunit zer            = refl _
  +ᶻ-lunit (pos zero)     = refl _
  +ᶻ-lunit (pos (succ x)) = ap zsucc (+ᶻ-lunit (pos x))
  +ᶻ-lunit (neg zero)     = refl _
  +ᶻ-lunit (neg (succ x)) = ap zpred (+ᶻ-lunit (neg x))


  +ᶻ-unit-zsucc : (n :)  zsucc n == (n +ᶻ pos zero)
  +ᶻ-unit-zsucc zer = refl _
  +ᶻ-unit-zsucc (pos zero) = refl _
  +ᶻ-unit-zsucc (pos (succ x)) = ap zsucc (+ᶻ-unit-zsucc (pos x))
  +ᶻ-unit-zsucc (neg zero) = refl _
  +ᶻ-unit-zsucc (neg (succ x)) = inv (zpredsucc-id (neg x)) · ap zpred (+ᶻ-unit-zsucc (neg x))

  +ᶻ-unit-zpred : (n :)  zpred n == (n +ᶻ neg zero)
  +ᶻ-unit-zpred zer = refl _
  +ᶻ-unit-zpred (pos zero) = refl zer
  +ᶻ-unit-zpred (pos (succ x)) = inv (zsuccpred-id (pos x)) · ap zsucc (+ᶻ-unit-zpred (pos x))
  +ᶻ-unit-zpred (neg zero) = refl _
  +ᶻ-unit-zpred (neg (succ x)) = ap zpred (+ᶻ-unit-zpred (neg x))


  +ᶻ-pos-zsucc : (n :)  (x :)  zsucc (n +ᶻ pos x) == n +ᶻ pos (succ x)
  +ᶻ-pos-zsucc zer x = refl _
  +ᶻ-pos-zsucc (pos zero) x = refl _
  +ᶻ-pos-zsucc (pos (succ n)) x = ap zsucc (+ᶻ-pos-zsucc (pos n) x)
  +ᶻ-pos-zsucc (neg zero) x = zsuccpred-id (pos x)
  +ᶻ-pos-zsucc (neg (succ n)) x = zsuccpred-predsucc (neg n +ᶻ pos x) · ap zpred (+ᶻ-pos-zsucc (neg n) x)

  +ᶻ-neg-zpred : (n :)  (x :)  zpred (n +ᶻ neg x) == n +ᶻ neg (succ x)
  +ᶻ-neg-zpred zer x = refl _
  +ᶻ-neg-zpred (pos zero) x = zpredsucc-id (neg x)
  +ᶻ-neg-zpred (pos (succ n)) x = zpredsucc-succpred (pos n +ᶻ neg x) · ap zsucc (+ᶻ-neg-zpred (pos n) x)
  +ᶻ-neg-zpred (neg zero) x = refl _
  +ᶻ-neg-zpred (neg (succ n)) x = ap zpred (+ᶻ-neg-zpred (neg n) x)

  +ᶻ-comm : (n m :)  n +ᶻ m == m +ᶻ n
  +ᶻ-comm zer m = +ᶻ-lunit m
  +ᶻ-comm (pos zero) m = +ᶻ-unit-zsucc m
  +ᶻ-comm (pos (succ x)) m = ap zsucc (+ᶻ-comm (pos x) m) · +ᶻ-pos-zsucc m x
  +ᶻ-comm (neg zero) m = +ᶻ-unit-zpred m
  +ᶻ-comm (neg (succ x)) m = ap zpred (+ᶻ-comm (neg x) m) · +ᶻ-neg-zpred m x



  -- Decidable equality
  pos-inj : {n m :}  pos n == pos m  n == m
  pos-inj {n} {.n} idp = refl n

  neg-inj : {n m :}  neg n == neg m  n == m
  neg-inj {n} {.n} idp = refl n

  z-decEq : decEq ℤ
  z-decEq zer zer = inl (refl zer)
  z-decEq zer (pos x) = inr (λ ())
  z-decEq zer (neg x) = inr (λ ())
  z-decEq (pos x) zer = inr (λ ())
  z-decEq (pos n) (pos m) with (nat-decEq n m)
  z-decEq (pos n) (pos m) | inl p = inl (ap pos p)
  z-decEq (pos n) (pos m) | inr f = inr (f ∘ pos-inj)
  z-decEq (pos n) (neg m) = inr (λ ())
  z-decEq (neg n) zer = inr (λ ())
  z-decEq (neg n) (pos x₁) = inr (λ ())
  z-decEq (neg n) (neg m) with (nat-decEq n m)
  z-decEq (neg n) (neg m) | inl p = inl (ap neg p)
  z-decEq (neg n) (neg m) | inr f = inr (f ∘ neg-inj)

  z-isSet : isSet ℤ
  z-isSet = hedberg z-decEq


  -- Multiplication
  infixl 60 _*ᶻ_
  _*ᶻ_ : ℤ
  zer *ᶻ m = zer
  pos zero *ᶻ m = m
  pos (succ x) *ᶻ m = (pos x *ᶻ m) +ᶻ m
  neg zero *ᶻ m = - m
  neg (succ x) *ᶻ m = (neg x *ᶻ m) +ᶻ (- m)


  -- Ordering
  _<ᶻ_ : Type₀
  zer <ᶻ zer = ⊥ lzero
  zer <ᶻ pos x = ⊤ lzero
  zer <ᶻ neg x = ⊥ lzero
  pos x <ᶻ zer = ⊥ lzero
  pos x <ᶻ pos y = x <ₙ y
  pos x <ᶻ neg y = ⊥ lzero
  neg x <ᶻ zer = ⊤ lzero
  neg x <ᶻ pos y = ⊤ lzero
  neg x <ᶻ neg y = y <ₙ x