module Cubical.Algebra.Group.Instances.Int where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Function

open import Cubical.Data.Int
  renaming (_+_ to _+ℤ_ ; _-_ to _-ℤ_; -_ to -ℤ_ ; _·_ to _·ℤ_)
open import Cubical.Data.Nat using (ℕ ; zero ; suc)
open import Cubical.Data.Fin.Inductive.Base

open import Cubical.Algebra.Group.Base
open import Cubical.Algebra.Group.Properties
open import Cubical.Algebra.Group.Morphisms
open import Cubical.Algebra.Group.MorphismProperties


open GroupStr

ℤGroup : Group₀
fst ℤGroup = ℤ
1g (snd ℤGroup) = 
_·_ (snd ℤGroup) = _+ℤ_
inv (snd ℤGroup) = -ℤ_
isGroup (snd ℤGroup) = isGroupℤ
  where
  abstract
    isGroupℤ : IsGroup (pos ) (_+ℤ_) (-ℤ_)
    isGroupℤ = makeIsGroup isSetℤ
                           +Assoc (λ _ → refl) (+Comm )
                           -Cancel -Cancel'

ℤHom : (n : ℤ) → GroupHom ℤGroup ℤGroup
fst (ℤHom n) x = n ·ℤ x
snd (ℤHom n) =
  makeIsGroupHom λ x y → ·DistR+ n x y

negEquivℤ : GroupEquiv ℤGroup ℤGroup
fst negEquivℤ =
  isoToEquiv
    (iso (GroupStr.inv (snd ℤGroup))
         (GroupStr.inv (snd ℤGroup))
         (GroupTheory.invInv ℤGroup)
         (GroupTheory.invInv ℤGroup))
snd negEquivℤ =
  makeIsGroupHom -Dist+

sumFinGroupℤComm : (G : Group₀) (h : GroupIso G ℤGroup) {n : ℕ}
  (f : Fin n → fst G) → sumFinℤ {n = n} (λ a → Iso.fun (fst h) (f a))
  ≡ Iso.fun (fst h) (sumFinGroup G {n = n} f)
sumFinGroupℤComm G h {n = zero} f = sym (IsGroupHom.pres1 (snd h))
sumFinGroupℤComm G h {n = suc n} f =
    cong₂ _+ℤ_ (λ _ → Iso.fun (fst h) (f flast))
      (sumFinGroupℤComm G h {n = n} (f ∘ injectSuc {n = n}))
  ∙ sym (IsGroupHom.pres· (snd h) (f flast)
    (sumFinGroup G {n = n} (λ x → f (injectSuc {n = n} x))))