Table of Contents

1 Prelude

2 Group definition

record Group (i : Level) : Type (lsuc i) where
    carrier : Type i
    op : carrier  carrier  carrier
    _^ᵍ : carrier  carrier
    e : carrier

    carrier-set : isSet carrier
    gp-assoc : (a b c : carrier)  op (op a b) c  op a (op b c)
    gp-lId : (a : carrier)  op e a  a
    gp-rId : (a : carrier)  op a e  a
    gp-lInv : (a : carrier)  op (a ^ᵍ) (a)  e
    gp-rInv : (a : carrier)  op a (a ^ᵍ)  e

  _og_ : carrier  carrier  carrier
  _og_ = op

  {- The identity is unique -}
  e-unique : (X : Σ[ e'  carrier ] (
             ((a : carrier)  op e' a  a) × (
             ((a : carrier)  op a e'  a) × (
             ((a : carrier)  op (a ^ᵍ) (a)  e) × (
             ((a : carrier)  op (a ^ᵍ) (a)  e))))))
              pr₁ X  e
  e-unique (e' , lId , rId , linv , rinv) =
    gp-lId e' ^  rId e

  {- The inverse of an element is unique -}
  inv-unique : (a : carrier)  (X : Σ[ b  carrier ] (
               (op b a  e) ×
               (op a b  e)))
                pr₁ X  (a ^ᵍ)
  inv-unique a (b , p , q) =
    gp-lId b ^ 
    transport  P  op P b  (a ^ᵍ)) (gp-lInv a)
      (gp-assoc (a ^ᵍ) a b 
      transport  P  op (a ^ᵍ) P  (a ^ᵍ)) (q ^)
        (gp-rId (a ^ᵍ)) )

  {- inverse is an involution -}
  inv-involution : (a : carrier)
                    (a ^ᵍ ) ^ᵍ  a
  inv-involution a =
      (a ^ᵍ)
      (a ,
      ((gp-rInv a) ,
       (gp-lInv a))) ^

  inv-of-prod : (a b : carrier)
                 (a og b) ^ᵍ  (b ^ᵍ) og (a ^ᵍ)
  inv-of-prod a b =
      (a og b)
      ((b ^ᵍ) og (a ^ᵍ) ,
      gp-assoc (b ^ᵍ) (a ^ᵍ) (a og b) 
        ap  z  op (b ^ᵍ) z) (gp-assoc (a ^ᵍ) a b ^) 
        ap  z  op (b ^ᵍ) (op z b)) (gp-lInv a) 
        ap  z  op (b ^ᵍ) z) (gp-lId b) 
        gp-lInv b ,
      gp-assoc a b ((b ^ᵍ) og (a ^ᵍ)) 
        ap  z  op a z) (gp-assoc b (b ^ᵍ) (a ^ᵍ) ^) 
        ap  z  op a (op z (a ^ᵍ))) (gp-rInv b) 
        ap  z  op a z) (gp-lId (a ^ᵍ)) 
        gp-rInv a) ^

  {- left and right cancellation laws -}
  gp-lCancel : (a b c : carrier)
                a og b  a og c
                b  c
  gp-lCancel a b c p =
    gp-lId b ^ 
    (ap  z  op z b) (gp-lInv a) ^ 
    (gp-assoc (a ^ᵍ) a b 
    ap  z  op (a ^ᵍ) z) p 
    gp-assoc (a ^ᵍ) a c ^) 
    ap  z  op z c) (gp-lInv a)) 
    gp-lId c

  gp-rCancel : (a b c : carrier)
                b og a  c og a
                b  c
  gp-rCancel a b c p =
    gp-rId b ^ 
    (ap  z  b og z) (gp-rInv a)) ^ 
    gp-assoc b a (a ^ᵍ) ^ 
    ap  z  op z (a ^ᵍ)) p 
    gp-assoc c a (a ^ᵍ) 
    ap  z  op c z) (gp-rInv a) 
    gp-rId c

2.1 Sigma definition

Group-sig : (i : Level)  Type (lsuc i)
Group-sig i =
  Σ[ carrier  (Type i) ](
    Σ[ op  (carrier  carrier  carrier) ] (
      Σ[ inv  (carrier  carrier) ] (
        Σ[ e  carrier ] (
          Σ[ carrier-set  (isSet carrier) ] (
           Σ[ gp-assoc  ((a b c : carrier)  op (op a b) c  op a (op b c)) ] (
             Σ[ gp-lId  ((a : carrier)  op e a  a) ] (
               Σ[ gp-rId  ((a : carrier)  op a e  a) ] (
                Σ[ gp-lInv  ((a : carrier)  op (inv a) a  e) ] (
                   (a : carrier)  op a (inv a)  e)))))))))
Group-sig→rec :  {i}
                 Group-sig i  Group i
Group.carrier (Group-sig→rec G) = pr₁ G
Group.op (Group-sig→rec G) = pr₁ (pr₂ G)
Group-sig→rec G Group.^ᵍ = pr₁ (pr₂ (pr₂ G))
Group.e (Group-sig→rec G) = pr₁ (pr₂ (pr₂ (pr₂ G)))
Group.carrier-set (Group-sig→rec G) = pr₁ (pr₂ (pr₂ (pr₂ (pr₂ G))))
Group.gp-assoc (Group-sig→rec G) = pr₁ (pr₂ (pr₂ (pr₂ (pr₂ (pr₂ G)))))
Group.gp-lId (Group-sig→rec G) = pr₁ (pr₂ (pr₂ (pr₂ (pr₂ (pr₂ (pr₂ G))))))
Group.gp-rId (Group-sig→rec G) = pr₁ (pr₂ (pr₂ (pr₂ (pr₂ (pr₂ (pr₂ (pr₂ G)))))))
Group.gp-lInv (Group-sig→rec G) = pr₁ (pr₂ (pr₂ (pr₂ (pr₂ (pr₂ (pr₂ (pr₂ (pr₂ G))))))))
Group.gp-rInv (Group-sig→rec G) = pr₂ (pr₂ (pr₂ (pr₂ (pr₂ (pr₂ (pr₂ (pr₂ (pr₂ G))))))))

Group-rec→sig :  {i}
                 Group i  Group-sig i
Group-rec→sig G =
  let module G = Group G in
  G.carrier ,
  G.op ,
  G._^ᵍ ,
  G.e ,
  G.carrier-set ,
  G.gp-assoc ,
  G.gp-lId ,
  G.gp-rId ,
  G.gp-lInv ,

Group-rec→sig→rec :  {i}
                    (G : Group i)
                     (Group-sig→rec o Group-rec→sig) G  G
Group-rec→sig→rec G = refl

Group-sig→rec→sig :  {i}
                    (G : Group-sig i)
                     (Group-rec→sig o Group-sig→rec) G  G
Group-sig→rec→sig G =
  path-equiv-sigma (refl ,
    path-equiv-sigma (refl ,
      (path-equiv-sigma (refl ,
        (path-equiv-sigma (refl ,
          (path-equiv-sigma (refl ,
            (path-equiv-sigma (refl ,
              (path-equiv-sigma (refl ,
                (path-equiv-sigma (refl ,
                  (path-equiv-sigma (refl ,

Group-sig-Equiv :  {i}
                   Group-sig i  Group i
Group-sig-Equiv = equiv-adjointify
  (Group-sig→rec ,
  Group-rec→sig ,
  Group-rec→sig→rec ,

3 Group homomorphism definition

4 Trivial Group

Author: James Leslie

Created: 2021-03-27 Sat 10:47