{-# OPTIONS --safe #-}
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) = 0
_·_ (snd ℤGroup) = _+ℤ_
inv (snd ℤGroup) = -ℤ_
isGroup (snd ℤGroup) = isGroupℤ
  where
  abstract
    isGroupℤ : IsGroup (pos 0) (_+ℤ_) (-ℤ_)
    isGroupℤ = makeIsGroup isSetℤ
                           +Assoc  _  refl) (+Comm 0)
                           -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))))