open import Level hiding ( suc ; zero )
module Gutil0  where

open import Algebra
open import Algebra.Structures
open import Algebra.Definitions
open import Data.Product
open import Relation.Binary.PropositionalEquality 
open import Algebra.Morphism.Structures
open import Data.Empty
open import Relation.Nullary

open GroupMorphisms

GR : {c l : Level } → Group c l → RawGroup c l
GR G = record {
     Carrier        = Carrier G
     ; _≈_          = _≈_ G
     ; _∙_          = _∙_ G
     ; ε            = ε G
     ; _⁻¹          = _⁻¹ G
  } where open Group

record GAxiom {c l : Level } (G : Group c l)  : Set ( c  Level.⊔  l ) where
  open Group G
  field
     ∙-cong :  {x y u v : Carrier } → x ≈ y → u ≈ v →  x ∙ u ≈  y ∙ v 
     assoc : (x y z : Carrier ) → x ∙ y ∙ z ≈  x ∙ ( y ∙ z )
     identity : ((y : Carrier) → ε ∙ y ≈ y ) ×  ((y : Carrier) → y ∙ ε ≈ y )
     inverse   : ((y : Carrier) → y ⁻¹ ∙ y  ≈ ε ) ×  ((y : Carrier) → y ∙ y ⁻¹  ≈ ε )
     ⁻¹-cong   : {x y : Carrier } → x ≈ y → x ⁻¹ ≈ y ⁻¹

GA : {c l : Level } → (G : Group c l) → GAxiom G
GA G = record {
        ∙-cong = IsMagma.∙-cong ( IsSemigroup.isMagma ( IsMonoid.isSemigroup ( IsGroup.isMonoid isGroup)))
     ;  assoc = IsSemigroup.assoc ( IsMonoid.isSemigroup ( IsGroup.isMonoid isGroup))
     ;  identity = IsMonoid.identity ( IsGroup.isMonoid isGroup)
     ;  inverse   = IsGroup.inverse isGroup
     ;  ⁻¹-cong   = IsGroup.⁻¹-cong isGroup
   } where open Group G

open import Relation.Binary.Structures

Eq : {c l : Level } → (G : Group c l) → IsEquivalence _
Eq G =  IsMagma.isEquivalence (IsSemigroup.isMagma (IsMonoid.isSemigroup
             (IsGroup.isMonoid (Group.isGroup G ))) )

grefl : {c l : Level } → (G : Group c l ) → {x : Group.Carrier G} → Group._≈_ G x x
grefl G = IsGroup.refl ( Group.isGroup G )

gsym : {c l : Level } → (G : Group c l ) → {x y : Group.Carrier G} → Group._≈_ G x y → Group._≈_ G y x
gsym G = IsGroup.sym ( Group.isGroup G )

gtrans : {c l : Level } → (G : Group c l ) → {x y z : Group.Carrier G} → Group._≈_ G x y → Group._≈_ G y z → Group._≈_ G x z
gtrans G = IsGroup.trans ( Group.isGroup G )

-- record NormalSubGroup {c l : Level } ( G : Group c l ) : Set ( c  Level.⊔  l ) where
--  open Group G
--  field
--     sub : Carrier → Carrier 
--     s-homo  : IsGroupHomomorphism (GR G) (GR G) sub
--     commute : ( g n : Carrier  ) → g ∙  sub n  ≈ sub n ∙ g
--     -- it has at least one element other than ε 
--     -- anElement : Carrier
--     -- notE : ¬ ( Group._≈_ G anElement (Group.ε G) )

-- open import Relation.Binary.Morphism.Structures

import Relation.Binary.Reasoning.Setoid as EqReasoning

-- record HomoMorphism {c l : Level } (G : Group c l) (f :  Group.Carrier G → Group.Carrier G) : Set ( c  Level.⊔  l ) where
--  open Group G
--  field
--     f-cong : {x y : Carrier } → x ≈ y → f x ≈ f y
--     f-homo : (x y : Carrier ) → f ( x ∙ y ) ≈ f x ∙ f y
--     f-ε : f ( ε ) ≈ ε
--     f-inv : (x : Carrier) → f ( x ⁻¹ ) ≈ (f x ) ⁻¹

-- HM : {c l : Level } → (G : Group c l ) → (f :  Group.Carrier G → Group.Carrier G )
--   → IsGroupHomomorphism (GR G) (GR G) f → HomoMorphism G f
-- HM G f homo = record {
--    f-cong = λ eq → IsRelHomomorphism.cong ( IsMagmaHomomorphism.isRelHomomorphism
--            ( IsMonoidHomomorphism.isMagmaHomomorphism ( IsGroupHomomorphism.isMonoidHomomorphism homo))) eq
--  ; f-homo = IsMagmaHomomorphism.homo (IsMonoidHomomorphism.isMagmaHomomorphism ( IsGroupHomomorphism.isMonoidHomomorphism homo))
--  ; f-ε  = IsMonoidHomomorphism.ε-homo ( IsGroupHomomorphism.isMonoidHomomorphism homo)
--  ; f-inv = IsGroupHomomorphism.⁻¹-homo homo
--  }
-- 
-- open HomoMorphism
-- 
-- hm : {c l : Level } → (G : Group c l ) → (f :  Group.Carrier G → Group.Carrier G )
--    → HomoMorphism G f
--    → IsGroupHomomorphism (GR G) (GR G) f
-- hm G f hm = record { isMonoidHomomorphism = record { isMagmaHomomorphism = record {
--              isRelHomomorphism = record { cong = λ {x} {y} eq → f-cong hm {x} {y} eq } 
--            ; homo =  f-homo hm } ; ε-homo =  f-ε hm } ; ⁻¹-homo = f-inv hm
--  } 
--