{-# 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  _⊗_
    _⊗_ = 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₂)