Integers

Groups.agda

{-# OPTIONS --type-in-type #-}
module _ where

open import Relation.Binary.HeterogeneousEquality
open ≅-Reasoning renaming (begin_ to proof_)
open import Function

record Group : Set₁ where
  field G    : Set
        e    : G
        op   : G → G → G
        inv  : G → G
        assp : ∀ a b c → op (op a b) c ≅ op a (op b c)
        linvp : ∀ a → op (inv a) a ≅ e
        rinvp : ∀ a → op a (inv a) ≅ e
        lidp : ∀ a → op e a ≅ a
        ridp : ∀ a → op a e ≅ a

open import Data.Nat renaming (_+_ to _ℕ+_) hiding (zero)
open import Data.Nat.Properties.Simple
open import Data.Product

Int = ℕ × ℕ -- (m , n) = m - n

_+_ : Int → Int → Int 
(x , y) + (x' , y') = x ℕ+ x' , y ℕ+ y'

-_ : Int → Int
- (x , y) = y , x


zero : Int
zero = 0 , 0

-- this one holds definitionally
lidp : ∀ i → zero + i ≅ i
lidp i = refl 

-- cong for pairs, useful for proving stuff about Ints using properties of ℕ
×Eq : {A B : Set}{a a' : A}{b b' : B} → a ≅ a' → b ≅ b' → a , b ≅ a' , b'
×Eq refl refl = refl

-- the next two follow from properties of ℕ+
ridp : ∀ i → i + zero ≅ i
ridp (x , y) = ×Eq (≡-to-≅ (+-right-identity x)) (≡-to-≅ (+-right-identity y))

assp : ∀ i j k → (i + j) + k ≅ i + (j + k)
assp (x , y) (x' , y') (x'' , y'') = ×Eq (≡-to-≅ (+-assoc x x' x'')) (≡-to-≅ (+-assoc y y' y''))

-- for invp we need a quotient, crudely represented here:
--postulate q : {x x' y y' : ℕ} → (x ℕ+ y' ≅ x' ℕ+ y) → (x , y ≅ x' , y')

-- a less crude quotient:

open import Relation.Binary

EqR : (A : Set) → Set₁
EqR A = Σ (Rel A _) (λ R → IsEquivalence R)

open IsEquivalence renaming (refl to irefl; sym to isym; trans to itrans)


record Quotient (A : Set) (R : EqR A) : Set where
  open Σ R renaming (proj₁ to _~_)
  field Q : Set
        abs : A → Q 

  compat : {B : Q → Set} → ((a : A) → B (abs a)) → Set
  compat f = ∀{a b} → a ~ b → f a ≅ f b
     
  field lift : {B : Q → Set}(f : (a : A) → B (abs a)) → (compat {B} f) →
               (q : Q) → B q
        ax1 : (a b : A) → a ~ b → abs a ≅ abs b
        ax2 : (a b : A) → abs a ≅ abs b → a ~ b
        ax3 : {B : Q → Set}(f : (a : A) → B (abs a))(p : compat {B} f)
               (a : A) → (lift {B} f p) (abs a) ≅ f a

postulate quot : (A : Set) (R : EqR A) → Quotient A R
postulate ext : {A : Set}{B B' : A → Set}{f : ∀ a → B a}{g : ∀ a → B' a} → 
                (∀ a → f a ≅ g a) → f ≅ g
postulate iext : {A : Set}{B B' : A → Set}{f : ∀ {a} → B a}{g : ∀{a} → B' a} → 
                 (∀ a → f {a} ≅ g {a}) → 
                 _≅_ {_}{ {a : A} → B a} f { {a : A} → B' a} g
fixtypes' : {A A' A'' A''' : Set}{a : A}{a' : A'}{a'' : A''}{a''' : A'''}
            {p : a ≅ a'}{q : a'' ≅ a'''} →
            a ≅ a'' → p ≅ q
fixtypes' {p = refl} {refl} refl = refl


compat₂ : ∀{A A' B}(R : EqR A)(R' : EqR A') → (A → A' → B) → Set
compat₂ R R' f = 
  let open Σ R renaming (proj₁ to _~_) 
      open Σ R' renaming (proj₁ to _≈_) 
  in ∀{a b a' b'} → a ~ a' → b ≈ b' → f a b ≅ f a' b'

conglift : ∀{A B}{R}{Q : Quotient A R}(f g : A → B) → 
  let open Quotient Q
      _∼_ , _ = R in
      (p : ∀{b b'} → b ∼ b' → f b ≅ f b') → 
      (p' : ∀{b b'} → b ∼ b' → g b ≅ g b') → 
      f ≅ g → 
      lift {λ _ → B} f p ≅ lift g p'
conglift {Q = Q} f .f p p' refl = 
 let open Quotient Q in cong 
     {x = λ{_ _} → p}
     {y = λ{_ _} → p'}
     (lift f) 
     (iext (λ _ → iext (λ _ → ext (λ _ → fixtypes' refl))))

lift₂ : ∀{A A' B R R'}(q : Quotient A R)(q' : Quotient A' R')
        (f : A → A' → B) → (compat₂ R R' f) → Quotient.Q q → Quotient.Q q' → B
lift₂ {A}{A'}{B}{R}{R'} q q' f p = 
  let open Σ R renaming (proj₁ to _~_; proj₂ to e) 
      open Σ R' renaming (proj₁ to _≈_; proj₂ to e')
      open Quotient q 
      open Quotient q' renaming (Q to Q'; abs to abs'; lift to lift')
  
      g : A → Q' → B
      g a = lift' (f a) (p (irefl e))

      fa≅fb : ∀{a b : A} → a ~ b → f a ≅ f b
      fa≅fb r = ext (λ a' → p r (irefl e'))

  in lift g (λ {a b} r → conglift {Q = q'}
    (f a) 
    (f b) 
    (p (irefl e)) 
    (p (irefl e)) 
    (fa≅fb r))

lift₂→lift : ∀{A A' B R R'}(q : Quotient A R)(q' : Quotient A' R')
             (f : A → A' → B)(p : compat₂ R R' f)(x : A)
             (x' : Quotient.Q q') → 
             lift₂ q q' f p (Quotient.abs q x) x' ≅ 
             Quotient.lift q' (f x) (p (IsEquivalence.refl (proj₂ R))) x' 
lift₂→lift {A}{A'}{B}{R}{R'} q q' f p x x' = 
  let open Σ R renaming (proj₁ to _~_; proj₂ to e) 
      open Σ R' renaming (proj₁ to _≈_; proj₂ to e')
      open Quotient q 
      open Quotient q' renaming (Q to Q'; 
                                 abs to abs'; 
                                 lift to lift'; 
                                 ax3 to ax3')
      s : ∀{a b} → a ~ b → 
          lift' (f a) (λ r → p (irefl e) r) ≅ lift' (f b) (λ r → p (irefl e) r)
      s {a}{b} r = conglift {Q = q'}
        (f a) 
        (f b) 
        (p (irefl e))
        (p (irefl e)) 
        (ext (λ _ → p r (irefl e'))) 

  in 
    proof
    lift (λ a → lift' (f a) (p (irefl e))) s (abs x) x'
    ≅⟨ cong (λ g → g x') (ax3 (λ a → lift' (f a) (p (irefl e))) s x) ⟩
    lift' (f x) (λ r → p (irefl e) r) x'
    ∎

lift₂absabs : ∀{A A' B R R'}(q : Quotient A R)(q' : Quotient A' R')
             (f : A → A' → B)(p : compat₂ R R' f)(x : A)(x' : A') → 
             lift₂ q q' f p (Quotient.abs q x) (Quotient.abs q' x') ≅ f x x'
lift₂absabs {R = R} q q' f p x x' = 
  let open Quotient q
      open Quotient q' renaming (abs to abs'; lift to lift'; ax3 to ax3' ) in
      proof
      lift₂ q q' f p (abs x) (abs' x')
      ≅⟨ lift₂→lift q q' f p x (abs' x') ⟩
      lift' (f x) (p (irefl (proj₂ R))) (abs' x') 
      ≅⟨ ax3' (f x) (p (irefl (proj₂ R))) x' ⟩
      f x x'
      ∎


_≅Int_ : Int → Int → Set
(x , y) ≅Int (x' , y') = x ℕ+ y' ≅ x' ℕ+ y

cong- : ∀ i i' → i ≅Int i' → - i ≅Int - i'
cong- (x , y)(x' , y') p = 
  proof 
  y ℕ+ x' 
  ≅⟨ ≡-to-≅ (+-comm y _) ⟩ 
  x' ℕ+ y 
  ≅⟨ sym p ⟩ 
  x ℕ+ y' 
  ≅⟨ ≡-to-≅ (+-comm x _) ⟩ 
  y' ℕ+ x 
  ∎

cong+ : ∀ i i' i'' i''' → i ≅Int i' → i'' ≅Int i''' → (i + i'') ≅Int (i' + i''')
cong+ (x , y) (x' , y') (x'' , y'') (x''' , y''') p q = 
  proof 
  (x ℕ+ x'') ℕ+ (y' ℕ+ y''') 
  ≅⟨ sym (≡-to-≅ (+-assoc (x ℕ+ x'') _ _)) ⟩ 
  ((x ℕ+ x'') ℕ+ y') ℕ+ y'''
  ≅⟨ cong (λ n → n ℕ+ y''') (≡-to-≅ (+-assoc x _ _)) ⟩ 
  (x ℕ+ (x'' ℕ+ y')) ℕ+ y'''
  ≅⟨ cong (λ n → x ℕ+ n ℕ+ y''') (≡-to-≅ (+-comm x'' _)) ⟩ 
  (x ℕ+ (y' ℕ+ x'')) ℕ+ y'''
  ≅⟨ cong (λ n → n ℕ+ y''') (sym (≡-to-≅ (+-assoc x _ _))) ⟩ 
  ((x ℕ+ y') ℕ+ x'') ℕ+ y'''
  ≅⟨ cong (λ n → n ℕ+ x'' ℕ+ y''') p ⟩ 
  ((x' ℕ+ y) ℕ+ x'') ℕ+ y'''
  ≅⟨ ≡-to-≅ (+-assoc (x' ℕ+ y) _ _) ⟩ 
  (x' ℕ+ y) ℕ+ (x'' ℕ+ y''')
  ≅⟨ cong (_ℕ+_ (x' ℕ+ y)) q ⟩
  (x' ℕ+ y) ℕ+ (x''' ℕ+ y'')
  ≅⟨ sym (≡-to-≅ (+-assoc (x' ℕ+ y) _ _)) ⟩ 
  ((x' ℕ+ y) ℕ+ x''') ℕ+ y''
  ≅⟨ cong (λ n → n ℕ+ y'') (≡-to-≅ (+-assoc x' _ _)) ⟩ 
  (x' ℕ+ (y ℕ+ x''')) ℕ+ y''
  ≅⟨ cong (λ n → x' ℕ+ n ℕ+ y'') (≡-to-≅ (+-comm y _)) ⟩ 
  (x' ℕ+ (x''' ℕ+ y)) ℕ+ y''
  ≅⟨ cong (λ n → n ℕ+ y'') (sym (≡-to-≅ (+-assoc x' _ _))) ⟩ 
  ((x' ℕ+ x''') ℕ+ y) ℕ+ y''
  ≅⟨ ≡-to-≅ (+-assoc (x' ℕ+ x''') _ _) ⟩ 
  (x' ℕ+ x''') ℕ+ (y ℕ+ y'') ∎


intrefl : ∀ i → i ≅Int i
intrefl i = refl

intsym : ∀ i i' → i ≅Int i' → i' ≅Int i
intsym i i' = sym

lem : ∀ {x x'} → suc x ≅ suc x' → x ≅ x'
lem refl = refl

lemma : ∀ {x x'} y → y ℕ+ x ≅ y ℕ+ x' → x ≅ x'
lemma ℕ.zero p  = p
lemma (suc y) p = lemma y (lem p)

inttrans : ∀ i i' i'' → i ≅Int i' → i' ≅Int i'' → i ≅Int i''
inttrans (x , y) (x' , y') (x'' , y'') p q = lemma x' $ 
  proof 
  x' ℕ+ (x ℕ+ y'') 
  ≅⟨ cong (_ℕ+_ x') (≡-to-≅ (+-comm x _)) ⟩ 
  x' ℕ+ (y'' ℕ+ x) 
  ≅⟨ sym (≡-to-≅ (+-assoc x' _ _)) ⟩ 
  (x' ℕ+ y'') ℕ+ x
  ≅⟨ cong (λ n → n ℕ+ x) q ⟩ 
  (x'' ℕ+ y') ℕ+ x
  ≅⟨ ≡-to-≅ (+-assoc x'' _ _) ⟩ 
  x'' ℕ+ (y' ℕ+ x)
  ≅⟨ cong (_ℕ+_ x'') (≡-to-≅ (+-comm y' _)) ⟩ 
  x'' ℕ+ (x ℕ+ y')
  ≅⟨ cong (_ℕ+_ x'') p ⟩ 
  x'' ℕ+ (x' ℕ+ y)
  ≅⟨ sym (≡-to-≅ (+-assoc x'' _ _)) ⟩ 
  (x'' ℕ+ x') ℕ+ y
  ≅⟨ cong (λ n → n ℕ+ y) (≡-to-≅ (+-comm x'' _)) ⟩ 
  (x' ℕ+ x'') ℕ+ y
  ≅⟨ ≡-to-≅ (+-assoc x' _ _) ⟩ 
  x' ℕ+ (x'' ℕ+ y) 
  ∎

IntEqR : EqR Int
IntEqR = _≅Int_ , record 
  { refl  = refl 
  ; sym   = sym 
  ; trans = λ {i i' i''} → inttrans i i' i'' }


open Quotient (quot Int IntEqR)

qzero : Q
qzero = abs zero

q-_ : Q → Q
q- i = lift (abs ∘ -_) (λ {i i'} p → ax1 _ _ (cong- i i' p)) i

_q+_ : Q → Q → Q
i q+ i' = lift₂ 
  (quot Int IntEqR)
  (quot Int IntEqR)
  (λ i i' → abs (i + i')) 
  (λ {i} {i'} {i''} {i'''} p q → ax1 _ _ (cong+ i i'' i' i''' p q)) 
  i 
  i'

linvp' : ∀ i → ((- i) + i) ≅Int zero
linvp' (x , y) = 
  proof 
  y ℕ+ x ℕ+ 0 
  ≅⟨ ≡-to-≅ (+-right-identity _) ⟩ 
  y ℕ+ x
  ≅⟨ ≡-to-≅ (+-comm y _) ⟩ 
  x ℕ+ y 
  ∎

linvp : ∀ i → (q- (abs i)) q+ (abs i) ≅ abs zero
linvp i = 
  proof 
  (q- abs i) q+ abs i 
  ≅⟨ cong (λ q → q q+ abs i) (ax3 (abs ∘ -_) 
                                  (λ {a} {b} p → ax1 _ _ (cong- a b p)) 
                                  i) ⟩ 
  (abs (- i)) q+ abs i 
  ≅⟨ lift₂absabs 
       (quot Int IntEqR) 
       (quot Int IntEqR)
       (λ i i' → abs (i + i')) 
       (λ {a b a' b'} p p' → ax1 _ _ (cong+ a a' b b' p p')) 
       (- i) 
       i ⟩ 
  abs ((- i) + i) 
  ≅⟨ ax1 _ _ (linvp' i) ⟩ 
  abs zero 
  ∎

{-
rinvp : ∀ i → i + (- i) ≅ zero
rinvp (x , y) = q (trans (+-right-identity _) (+-comm x _))
-}

IntGrp : Group
IntGrp = record
  { G    = Q
  ; e    = qzero
  ; op   = _q+_
  ; inv  = q-_
  ; assp = {!!}
  ; linvp = lift {λ z → (q- z) q+ z ≅ qzero} linvp {!!}
  ; rinvp = {!!}
  ; ridp = {!!}
  ; lidp = {!!}
  }