{-# OPTIONS --safe #-}
module Cubical.Algebra.Group.Base where
{-
  Defines groups and adds the smart constructors [makeGroup-right] and [makeGroup-left]
  for constructing groups from less data than the standard [makeGroup] constructor.
-}

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Structure
open import Cubical.Data.Sigma
open import Cubical.Data.Nat using ()
open import Cubical.Data.Fin.Inductive.Base
open import Cubical.Algebra.Monoid
open import Cubical.Algebra.Semigroup

open import Cubical.Reflection.RecordEquiv


private
  variable
     : Level

record IsGroup {G : Type }
               (1g : G) (_·_ : G  G  G) (inv : G  G) : Type  where

  constructor isgroup

  field
    isMonoid  : IsMonoid 1g _·_
    ·InvR : (x : G)  x · inv x  1g
    ·InvL : (x : G)  inv x · x  1g

  open IsMonoid isMonoid public

unquoteDecl IsGroupIsoΣ = declareRecordIsoΣ IsGroupIsoΣ (quote IsGroup)

record GroupStr (G : Type ) : Type  where

  constructor groupstr

  field
    1g      : G
    _·_     : G  G  G
    inv     : G  G
    isGroup : IsGroup 1g _·_ inv

  infixr 7 _·_

  open IsGroup isGroup public

unquoteDecl GroupStrIsoΣ = declareRecordIsoΣ GroupStrIsoΣ (quote GroupStr)

Group :    Type (ℓ-suc )
Group  = TypeWithStr  GroupStr

Group₀ : Type₁
Group₀ = Group ℓ-zero

group : (G : Type ) (1g : G) (_·_ : G  G  G) (inv : G  G) (h : IsGroup 1g _·_ inv)  Group 
group G 1g _·_ inv h = G , groupstr 1g _·_ inv h

makeIsGroup : {G : Type } {e : G} {_·_ : G  G  G} { inv : G  G}
              (is-setG : isSet G)
              (·Assoc : (x y z : G)  x · (y · z)  (x · y) · z)
              (·IdR : (x : G)  x · e  x)
              (·IdL : (x : G)  e · x  x)
              (·InvR : (x : G)  x · inv x  e)
              (·InvL : (x : G)  inv x · x  e)
             IsGroup e _·_ inv
IsGroup.isMonoid (makeIsGroup is-setG ·Assoc ·IdR ·IdL ·InvR ·InvL) = makeIsMonoid is-setG ·Assoc ·IdR ·IdL
IsGroup.·InvR (makeIsGroup is-setG ·Assoc ·IdR ·IdL ·InvR ·InvL) = ·InvR
IsGroup.·InvL (makeIsGroup is-setG ·Assoc ·IdR ·IdL ·InvR ·InvL) = ·InvL

makeGroup : {G : Type } (1g : G) (_·_ : G  G  G) (inv : G  G)
            (is-setG : isSet G)
            (·Assoc : (x y z : G)  x · (y · z)  (x · y) · z)
            (·IdR : (x : G)  x · 1g  x)
            (·IdL : (x : G)  1g · x  x)
            (·InvR : (x : G)  x · inv x  1g)
            (·InvL : (x : G)  inv x · x  1g)
           Group 
makeGroup 1g _·_ inv is-setG ·Assoc ·IdR ·IdL ·InvR ·InvL = _ , helper
  where
  helper : GroupStr _
  GroupStr.1g helper = 1g
  GroupStr._·_ helper = _·_
  GroupStr.inv helper = inv
  GroupStr.isGroup helper = makeIsGroup is-setG ·Assoc ·IdR ·IdL ·InvR ·InvL

Group→Monoid : Group   Monoid 
Group→Monoid (A , groupstr  _ _ _ G) = A , monoidstr _ _ (IsGroup.isMonoid G)

makeGroup-right : {A : Type }
   (1g : A)
   (_·_ : A  A  A)
   (inv : A  A)
   (set : isSet A)
   (·Assoc :  a b c  a · (b · c)  (a · b) · c)
   (·IdR :  a  a · 1g  a)
   (·InvR :  a  a · inv a  1g)
   Group 
makeGroup-right 1g _·_ inv set ·Assoc ·IdR ·InvR =
  makeGroup 1g _·_ inv set ·Assoc ·IdR ·IdL ·InvR ·InvL
  where
    abstract
      ·InvL :  a  inv a · a  1g
      ·InvL a =
        inv a · a
          ≡⟨ sym (·IdR _)  
        (inv a · a) · 1g
          ≡⟨ cong (_·_ _) (sym (·InvR (inv a))) 
        (inv a · a) · (inv a · (inv (inv a)))
          ≡⟨ ·Assoc _ _ _ 
        ((inv a · a) · (inv a)) · (inv (inv a))
          ≡⟨ cong     · _) (sym (·Assoc _ _ _)) 
        (inv a · (a · inv a)) · (inv (inv a))
          ≡⟨ cong    (inv a · ) · (inv (inv a))) (·InvR a) 
        (inv a · 1g) · (inv (inv a))
          ≡⟨ cong     · (inv (inv a))) (·IdR (inv a)) 
        inv a · (inv (inv a))
          ≡⟨ ·InvR (inv a) 
        1g
          

      ·IdL :  a  1g · a  a
      ·IdL a =
        1g · a
          ≡⟨ cong  b  b · a) (sym (·InvR a)) 
        (a · inv a) · a
          ≡⟨ sym (·Assoc _ _ _) 
        a · (inv a · a)
          ≡⟨ cong (a ·_) (·InvL a) 
        a · 1g
          ≡⟨ ·IdR a 
        a
          

makeGroup-left : {A : Type }
   (1g : A)
   (_·_ : A  A  A)
   (inv : A  A)
   (set : isSet A)
   (·Assoc :  a b c  a · (b · c)  (a · b) · c)
   (·IdL :  a  1g · a  a)
   (·InvL :  a  (inv a) · a  1g)
   Group 
makeGroup-left 1g _·_ inv set ·Assoc ·IdL ·InvL =
  makeGroup 1g _·_ inv set ·Assoc ·IdR ·IdL ·InvR ·InvL
  where
    abstract
      ·InvR :  a  a · inv a  1g
      ·InvR a =
        a · inv a
          ≡⟨ sym (·IdL _)  
        1g · (a · inv a)
          ≡⟨ cong  b  b · (a · inv a)) (sym (·InvL (inv a))) 
        (inv (inv a) · inv a) · (a · inv a)
          ≡⟨ sym (·Assoc (inv (inv a)) (inv a) _) 
        inv (inv a) · (inv a · (a · inv a))
          ≡⟨ cong (inv (inv a) ·_) (·Assoc (inv a) a (inv a)) 
        (inv (inv a)) · ((inv a · a) · (inv a))
          ≡⟨ cong  b  (inv (inv a)) · (b · (inv a))) (·InvL a) 
        inv (inv a) · (1g · inv a)
          ≡⟨ cong (inv (inv a) ·_) (·IdL (inv a)) 
        inv (inv a) · inv a
          ≡⟨ ·InvL (inv a) 
        1g
          

      ·IdR :  a  a · 1g  a
      ·IdR a =
        a · 1g
          ≡⟨ cong (a ·_) (sym (·InvL a)) 
        a · (inv a · a)
          ≡⟨ ·Assoc a (inv a) a 
        (a · inv a) · a
          ≡⟨ cong  b  b · a) (·InvR a) 
        1g · a
          ≡⟨ ·IdL a 
        a
          

sumFinGroup :  {} (G : Group ) {n : } (f : Fin n  fst G)  fst G
sumFinGroup G {n = n} f = sumFinGen {n = n} (GroupStr._·_ (snd G)) (GroupStr.1g (snd G)) f