{-# OPTIONS --without-K #-}

open import lib.Basics
open import lib.types.Group
open import lib.types.Pi
open import lib.types.Sigma
open import lib.types.Truncation
open import lib.groups.GroupProduct
open import lib.groups.Homomorphisms

module lib.groups.TruncationGroup where

module _ {i} {El : Type i} (GS : GroupStructure El) where

  Trunc-group-struct : GroupStructure (Trunc ⟨0⟩ El)
  Trunc-group-struct = record {
    ident = [ ident GS ];
    inv = Trunc-fmap (inv GS);
    comp = _⊗_;
    unitl = t-unitl;
    unitr = t-unitr;
    assoc = t-assoc;
    invl = t-invl;
    invr = t-invr}
    where
    open GroupStructure
    infix 80 _⊗_
    _⊗_ = Trunc-fmap2 (comp GS)

    abstract
      t-unitl : (t : Trunc ⟨0⟩ El)  [ ident GS ]  t == t
      t-unitl = Trunc-elim  _  =-preserves-level _ Trunc-level)
        (ap [_]  unitl GS)

      t-unitr : (t : Trunc ⟨0⟩ El)  t  [ ident GS ] == t
      t-unitr = Trunc-elim  _  =-preserves-level _ Trunc-level)
        (ap [_]  unitr GS)

      t-assoc : (t₁ t₂ t₃ : Trunc ⟨0⟩ El)  (t₁  t₂)  t₃ == t₁  (t₂  t₃)
      t-assoc = Trunc-elim
         _  Π-level  _  Π-level  _  =-preserves-level _ Trunc-level)))
         a  Trunc-elim
           _  Π-level  _  =-preserves-level _ Trunc-level))
           b  Trunc-elim
              _  =-preserves-level _ Trunc-level)
              c  ap [_] (assoc GS a b c))))

      t-invl : (t : Trunc ⟨0⟩ El)  Trunc-fmap (inv GS) t  t == [ ident GS ]
      t-invl = Trunc-elim  _  =-preserves-level _ Trunc-level)
        (ap [_]  invl GS)

      t-invr : (t : Trunc ⟨0⟩ El)  t  Trunc-fmap (inv GS) t == [ ident GS ]
      t-invr = Trunc-elim  _  =-preserves-level _ Trunc-level)
        (ap [_]  invr GS)


  Trunc-Group : Group i
  Trunc-Group = record {
    El = Trunc ⟨0⟩ El;
    El-level = Trunc-level;
    group-struct = Trunc-group-struct }

Trunc-Group-× :  {i j} {A : Type i} {B : Type j}
  (GS : GroupStructure A) (HS : GroupStructure B)
   Trunc-Group (×-group-struct GS HS) == Trunc-Group GS ×ᴳ Trunc-Group HS
Trunc-Group-× GS HS = group-ua
  (record {
    f = Trunc-rec (×-level Trunc-level Trunc-level)
           {(a , b)  ([ a ] , [ b ])});
    pres-comp =
      Trunc-elim
         _  (Π-level  _  =-preserves-level _
                                 (×-level Trunc-level Trunc-level))))
         a  Trunc-elim
           _  =-preserves-level _ (×-level Trunc-level Trunc-level))
           b  idp))} ,
   is-eq _
    (uncurry (Trunc-rec (→-level Trunc-level)
                a  Trunc-rec Trunc-level  b  [ a , b ]))))
    (uncurry (Trunc-elim
                _  Π-level  _  =-preserves-level _
                                       (×-level Trunc-level Trunc-level)))
                a  Trunc-elim
                         _  =-preserves-level _
                                 (×-level Trunc-level Trunc-level))
                         b  idp))))
    (Trunc-elim  _  =-preserves-level _ Trunc-level)  _  idp)))

Trunc-Group-hom :  {i j} {A : Type i} {B : Type j}
  {GS : GroupStructure A} {HS : GroupStructure B} (f : A  B)
   ((a₁ a₂ : A)  f (GroupStructure.comp GS a₁ a₂)
                   == GroupStructure.comp HS (f a₁) (f a₂))
   (Trunc-Group GS →ᴳ Trunc-Group HS)
Trunc-Group-hom {A = A} {GS = GS} {HS = HS} f p =
  record {f = Trunc-fmap f; pres-comp = pres-comp}
  where
  abstract
    pres-comp : (t₁ t₂ : Trunc ⟨0⟩ A) 
      Trunc-fmap f (Trunc-fmap2 (GroupStructure.comp GS) t₁ t₂)
      == Trunc-fmap2 (GroupStructure.comp HS)
           (Trunc-fmap f t₁) (Trunc-fmap f t₂)
    pres-comp =
      Trunc-elim  _  Π-level  _  =-preserves-level _ Trunc-level))
         a₁  Trunc-elim  _  =-preserves-level _ Trunc-level)
           a₂  ap [_] (p a₁ a₂)))

Trunc-Group-iso :  {i} {A B : Type i}
  {GS : GroupStructure A} {HS : GroupStructure B} (f : A  B)
   ((a₁ a₂ : A)  f (GroupStructure.comp GS a₁ a₂)
                   == GroupStructure.comp HS (f a₁) (f a₂))
   is-equiv f  Trunc-Group GS ≃ᴳ Trunc-Group HS
Trunc-Group-iso f pres-comp ie =
  (Trunc-Group-hom f pres-comp ,
   is-eq _ (Trunc-fmap (is-equiv.g ie))
     (Trunc-elim  _  =-preserves-level _ Trunc-level)
        b  ap [_] (is-equiv.f-g ie b)))
     (Trunc-elim  _  =-preserves-level _ Trunc-level)
        a  ap [_] (is-equiv.g-f ie a))))

Trunc-Group-abelian :  {i} {A : Type i} (GS : GroupStructure A)
   ((a₁ a₂ : A)  GroupStructure.comp GS a₁ a₂ == GroupStructure.comp GS a₂ a₁)
   is-abelian (Trunc-Group GS)
Trunc-Group-abelian GS ab =
  Trunc-elim  _  Π-level  _  =-preserves-level _ Trunc-level)) $
    λ a₁  Trunc-elim  _  =-preserves-level _ Trunc-level) $
      λ a₂  ap [_] (ab a₁ a₂)