lib.groups.Isomorphism

{-# OPTIONS --without-K --rewriting --overlapping-instances #-}

open import lib.Basics
open import lib.Equivalence2
open import lib.Function2
open import lib.NType2
open import lib.FTID
open import lib.Funext2
open import lib.types.Unit
open import lib.types.Group
open import lib.types.Pi
open import lib.types.Sigma
open import lib.types.Subtype
open import lib.types.Truncation
open import lib.groups.Homomorphism

module lib.groups.Isomorphism where

GroupStructureIso : ∀ {i j} {GEl : Type i} {HEl : Type j}
  (GS : GroupStructure GEl) (HS : GroupStructure HEl) → Type (lmax i j)
GroupStructureIso GS HS = Σ (GroupStructureHom GS HS) (λ φ → is-equiv (GroupStructureHom.f φ))

infix 30 _≃ᴳˢ_ -- [ˢ] for structures
_≃ᴳˢ_ = GroupStructureIso

GroupIso : ∀ {i j} (G : Group i) (H : Group j) → Type (lmax i j)
GroupIso G H = Σ (G →ᴳ H) (λ φ → is-equiv (GroupHom.f φ))

infix 30 _≃ᴳ_
_≃ᴳ_ = GroupIso

≃ᴳˢ-to-≃ᴳ : ∀ {i j} {G : Group i} {H : Group j}
  → (Group.group-struct G ≃ᴳˢ Group.group-struct H) → (G ≃ᴳ H)
≃ᴳˢ-to-≃ᴳ (φ , φ-is-equiv) = →ᴳˢ-to-→ᴳ φ , φ-is-equiv

≃-to-≃ᴳ : ∀ {i j} {G : Group i} {H : Group j} (e : Group.El G ≃ Group.El H)
  → preserves-comp (Group.comp G) (Group.comp H) (–> e) → G ≃ᴳ H
≃-to-≃ᴳ (f , f-is-equiv) pres-comp = group-hom f pres-comp , f-is-equiv

≃-to-≃ᴳˢ : ∀ {i j} {GEl : Type i} {HEl : Type j}
  {GS : GroupStructure GEl} {HS : GroupStructure HEl} (e : GEl ≃ HEl)
  → preserves-comp (GroupStructure.comp GS) (GroupStructure.comp HS) (–> e)
  → GS ≃ᴳˢ HS
≃-to-≃ᴳˢ (f , f-is-equiv) pres-comp = group-structure-hom f pres-comp , f-is-equiv

private
  inverse-preserves-comp : ∀ {i j} {A : Type i} {B : Type j}
    (A-comp : A → A → A) (B-comp : B → B → B) {f : A → B} (f-ie : is-equiv f)
    → preserves-comp A-comp B-comp f
    → preserves-comp B-comp A-comp (is-equiv.g f-ie)
  inverse-preserves-comp Ac Bc ie pc b₁ b₂ = let open is-equiv ie in
    ap2 (λ w₁ w₂ → g (Bc w₁ w₂)) (! (f-g b₁)) (! (f-g b₂))
    ∙ ! (ap g (pc (g b₁) (g b₂)))
    ∙ g-f (Ac (g b₁) (g b₂))

module GroupStructureIso {i j} {GEl : Type i} {HEl : Type j}
  {GS : GroupStructure GEl} {HS : GroupStructure HEl}
  (iso : GroupStructureIso GS HS) where

  f-shom : GS →ᴳˢ HS
  f-shom = fst iso

  open GroupStructureHom {GS = GS} {HS = HS} f-shom public

  f-is-equiv : is-equiv f
  f-is-equiv = snd iso

  open is-equiv f-is-equiv public

  f-equiv : GEl ≃ HEl
  f-equiv = f , f-is-equiv

  g-shom : HS →ᴳˢ GS
  g-shom = group-structure-hom g (inverse-preserves-comp (GroupStructure.comp GS) (GroupStructure.comp HS) f-is-equiv pres-comp)

  g-is-equiv : is-equiv g
  g-is-equiv = is-equiv-inverse f-is-equiv

  g-equiv : HEl ≃ GEl
  g-equiv = g , g-is-equiv

module GroupIso {i j} {G : Group i} {H : Group j} (iso : GroupIso G H) where

  f-hom : G →ᴳ H
  f-hom = fst iso

  open GroupHom {G = G} {H = H} f-hom public

  f-is-equiv : is-equiv f
  f-is-equiv = snd iso

  open is-equiv f-is-equiv public

  f-equiv : Group.El G ≃ Group.El H
  f-equiv = f , f-is-equiv

  ⊙f-equiv : Group.⊙El G ⊙≃ Group.⊙El H
  ⊙f-equiv = ≃-to-⊙≃ f-equiv pres-ident

  g-hom : H →ᴳ G
  g-hom = group-hom g (inverse-preserves-comp (Group.comp G) (Group.comp H) f-is-equiv pres-comp)

  g-is-equiv : is-equiv g
  g-is-equiv = is-equiv-inverse f-is-equiv

  g-equiv : Group.El H ≃ Group.El G
  g-equiv = g , g-is-equiv

idiso : ∀ {i} (G : Group i) → (G ≃ᴳ G)
idiso G = idhom G , idf-is-equiv _

idsiso : ∀ {i} {GEl : Type i} (GS : GroupStructure GEl) → (GS ≃ᴳˢ GS)
idsiso GS = idshom GS , idf-is-equiv _

{- equality of isomomorphisms -}
abstract
  group-hom=-to-iso= : ∀ {i j} {G : Group i} {H : Group j} {φ ψ : G ≃ᴳ H}
    → GroupIso.f-hom φ == GroupIso.f-hom ψ → φ == ψ
  group-hom=-to-iso= = Subtype=-out (is-equiv-prop ∘sub GroupHom.f)

  group-iso= : ∀ {i j} {G : Group i} {H : Group j} {φ ψ : G ≃ᴳ H}
    → GroupIso.f φ == GroupIso.f ψ → φ == ψ
  group-iso= {H = H} p = group-hom=-to-iso= $ group-hom= p

{- compositions -}

infixr 80 _∘eᴳˢ_ _∘eᴳ_

_∘eᴳˢ_ : ∀ {i j k} {GEl : Type i} {HEl : Type j} {KEl : Type k}
  {GS : GroupStructure GEl} {HS : GroupStructure HEl} {KS : GroupStructure KEl}
  → HS ≃ᴳˢ KS → GS ≃ᴳˢ HS → GS ≃ᴳˢ KS
(φ₂ , ie₂) ∘eᴳˢ (φ₁ , ie₁) = (φ₂ ∘ᴳˢ φ₁ , ie₂ ∘ise ie₁)

_∘eᴳ_ : ∀ {i j k} {G : Group i} {H : Group j} {K : Group k}
  → H ≃ᴳ K → G ≃ᴳ H → G ≃ᴳ K
(φ₂ , ie₂) ∘eᴳ (φ₁ , ie₁) = (φ₂ ∘ᴳ φ₁ , ie₂ ∘ise ie₁)

infixr 10 _≃ᴳˢ⟨_⟩_ _≃ᴳ⟨_⟩_
infix  15 _≃ᴳˢ∎ _≃ᴳ∎

_≃ᴳˢ⟨_⟩_ : ∀ {i j k} {GEl : Type i} {HEl : Type j} {KEl : Type k}
  (GS : GroupStructure GEl) {HS : GroupStructure HEl} {KS : GroupStructure KEl}
  → GS ≃ᴳˢ HS → HS ≃ᴳˢ KS → GS ≃ᴳˢ KS
GS ≃ᴳˢ⟨ e₁ ⟩ e₂ = e₂ ∘eᴳˢ e₁

_≃ᴳ⟨_⟩_ : ∀ {i j k} (G : Group i) {H : Group j} {K : Group k}
  → G ≃ᴳ H → H ≃ᴳ K → G ≃ᴳ K
G ≃ᴳ⟨ e₁ ⟩ e₂ = e₂ ∘eᴳ e₁

_≃ᴳˢ∎ : ∀ {i} {GEl : Type i} (GS : GroupStructure GEl) → (GS ≃ᴳˢ GS)
_≃ᴳˢ∎ = idsiso

_≃ᴳ∎ : ∀ {i} (G : Group i) → (G ≃ᴳ G)
_≃ᴳ∎ = idiso

infixl 120 _⁻¹ᴳˢ _⁻¹ᴳ

_⁻¹ᴳˢ : ∀ {i j} {GEl : Type i} {HEl : Type j} {GS : GroupStructure GEl} {HS : GroupStructure HEl}
  → GS ≃ᴳˢ HS → HS ≃ᴳˢ GS
_⁻¹ᴳˢ {GS = GS} {HS} (φ , ie) = GroupStructureIso.g-shom (φ , ie) , is-equiv-inverse ie

_⁻¹ᴳ : ∀ {i j} {G : Group i} {H : Group j} → G ≃ᴳ H → H ≃ᴳ G
_⁻¹ᴳ {G = G} {H = H} (φ , ie) = GroupIso.g-hom (φ , ie) , is-equiv-inverse ie

{- mimicking notations for equivalences -}

–>ᴳ : ∀ {i j} {G : Group i} {H : Group j} → (G ≃ᴳ H) → (G →ᴳ H)
–>ᴳ = GroupIso.f-hom

<–ᴳ : ∀ {i j} {G : Group i} {H : Group j} → (G ≃ᴳ H) → (H →ᴳ G)
<–ᴳ = GroupIso.g-hom

{- univalence -}

module _ {i} {G H : Group i} (iso : GroupIso G H) where
  private
    module G = Group G
    module H = Group H
    open module φ = GroupIso {G = G} {H = H} iso
  El= = ua f-equiv

  private
    ap3-lemma : ∀ {i j k l} {C : Type i} {D : C → Type j} {E : C → Type k}
      {F : Type l} {c₁ c₂ : C} {d₁ : D c₁} {d₂ : D c₂} {e₁ : E c₁} {e₂ : E c₂}
      (f : (c : C) → D c → E c → F) (p : c₁ == c₂)
      → (d₁ == d₂ [ D ↓ p ]) → (e₁ == e₂ [ E ↓ p ])
      → (f c₁ d₁ e₁ == f c₂ d₂ e₂)
    ap3-lemma f idp idp idp = idp

    ap3-lemma-El : ∀ {i} {G H : Group i}
      (p : Group.El G == Group.El H)
      (q : Group.El-level G == Group.El-level H [ _ ↓ p ])
      (r : Group.group-struct G == Group.group-struct H [ _ ↓ p ])
      → ap Group.El (ap3-lemma (λ a b c → group a {{b}} c) p q r) == p
    ap3-lemma-El idp idp idp = idp

  {- a homomorphism which is an equivalence gives a path between groups -}
  abstract
    uaᴳ : G == H
    uaᴳ =
      ap3-lemma (λ a b c → group a {{b}} c)
        El=
        prop-has-all-paths-↓
        (↓-group-structure= El= ident= inv= comp=)
      where
      ident= : G.ident == H.ident [ (λ C → C) ↓ El= ]
      ident= = ↓-idf-ua-in _ pres-ident

      inv= : G.inv == H.inv [ (λ C → C → C) ↓ El= ]
      inv= =
        ↓-→-from-transp $ λ= λ a →
          transport (λ C → C) El= (G.inv a)
            =⟨ to-transp (↓-idf-ua-in _ idp) ⟩
          f (G.inv a)
            =⟨ pres-inv a ⟩
          H.inv (f a)
            =⟨ ap H.inv (! (to-transp (↓-idf-ua-in _ idp))) ⟩
          H.inv (transport (λ C → C) El= a) =∎

      comp=' : (a : G.El)
        → G.comp a == H.comp (f a) [ (λ C → C → C) ↓ El= ]
      comp=' a =
        ↓-→-from-transp $ λ= λ b →
          transport (λ C → C) El= (G.comp a b)
            =⟨ to-transp (↓-idf-ua-in _ idp) ⟩
          f (G.comp a b)
            =⟨ pres-comp a b ⟩
          H.comp (f a) (f b)
            =⟨ ! (to-transp (↓-idf-ua-in _ idp))
               |in-ctx (λ w → H.comp (f a) w) ⟩
          H.comp (f a) (transport (λ C → C) El= b) =∎

      comp= : G.comp == H.comp [ (λ C → C → C → C) ↓ El= ]
      comp= =
        ↓-→-from-transp $ λ= λ a →
          transport (λ C → C → C) El= (G.comp a)
            =⟨ to-transp (comp=' a) ⟩
          H.comp (f a)
            =⟨ ! (to-transp (↓-idf-ua-in _ idp)) |in-ctx (λ w → H.comp w) ⟩
          H.comp (transport (λ C → C) El= a) =∎

    -- XXX This stretches the naming convention a little bit.
    El=-β : ap Group.El uaᴳ == El=
    El=-β = ap3-lemma-El El= _ _

module _ {i} {G H : AbGroup i} (iso : GroupIso (fst G) (fst H)) where
  private
    module Gm = AbGroup G
    module Hm = AbGroup H

  abstract
    uaᴳ-Ab : G == H
    uaᴳ-Ab = pair= (uaᴳ iso) prop-has-all-paths-↓

{- homomorphism from equality of groups -}

abstract
  transp-El-pres-comp : ∀ {i j} {A : Type i} (B : A → Group j) {a₁ a₂ : A} (p : a₁ == a₂)
    → preserves-comp (Group.comp (B a₁)) (Group.comp (B a₂)) (transport (Group.El ∘ B) p)
  transp-El-pres-comp B idp g₁ g₂ = idp

  transp!-El-pres-comp : ∀ {i j} {A : Type i} (B : A → Group j) {a₁ a₂ : A} (p : a₁ == a₂)
    → preserves-comp (Group.comp (B a₂)) (Group.comp (B a₁)) (transport! (Group.El ∘ B) p)
  transp!-El-pres-comp B idp h₁ h₂ = idp

transportᴳ : ∀ {i j} {A : Type i} (B : A → Group j) {a₁ a₂ : A} (p : a₁ == a₂)
  → (B a₁ →ᴳ B a₂)
transportᴳ B p = record {f = transport (Group.El ∘ B) p; pres-comp = transp-El-pres-comp B p}

transport!ᴳ : ∀ {i j} {A : Type i} (B : A → Group j) {a₁ a₂ : A} (p : a₁ == a₂)
  → (B a₂ →ᴳ B a₁)
transport!ᴳ B p = record {f = transport! (Group.El ∘ B) p; pres-comp = transp!-El-pres-comp B p}

abstract
  transpᴳ-is-iso : ∀ {i j} {A : Type i} (B : A → Group j) {a₁ a₂ : A} (p : a₁ == a₂)
    → is-equiv (GroupHom.f (transportᴳ B p))
  transpᴳ-is-iso B idp = idf-is-equiv _

  transp!ᴳ-is-iso : ∀ {i j} {A : Type i} (B : A → Group j) {a₁ a₂ : A} (p : a₁ == a₂)
    → is-equiv (GroupHom.f (transport!ᴳ B p))
  transp!ᴳ-is-iso B idp = idf-is-equiv _

transportᴳ-iso : ∀ {i j} {A : Type i} (B : A → Group j) {a₁ a₂ : A} (p : a₁ == a₂)
  → B a₁ ≃ᴳ B a₂
transportᴳ-iso B p = transportᴳ B p , transpᴳ-is-iso B p

transport!ᴳ-iso : ∀ {i j} {A : Type i} (B : A → Group j) {a₁ a₂ : A} (p : a₁ == a₂)
  → B a₂ ≃ᴳ B a₁
transport!ᴳ-iso B p = transport!ᴳ B p , transp!ᴳ-is-iso B p

coeᴳ : ∀ {i} {G H : Group i} → G == H → (G →ᴳ H)
coeᴳ = transportᴳ (idf _)

coe!ᴳ : ∀ {i} {G H : Group i} → G == H → (H →ᴳ G)
coe!ᴳ = transport!ᴳ (idf _)

coeᴳ-iso : ∀ {i} {G H : Group i} → G == H → G ≃ᴳ H
coeᴳ-iso = transportᴳ-iso (idf _)

coe!ᴳ-iso : ∀ {i} {G H : Group i} → G == H → H ≃ᴳ G
coe!ᴳ-iso = transport!ᴳ-iso (idf _)

abstract
  coeᴳ-β : ∀ {i} {G H : Group i} (iso : G ≃ᴳ H)
    → coeᴳ (uaᴳ iso) == GroupIso.f-hom iso
  coeᴳ-β iso = group-hom= $
      ap coe (El=-β iso)
    ∙ λ= (coe-β (GroupIso.f-equiv iso))

-- triviality

iso-preserves-trivial : ∀ {i j} {G : Group i} {H : Group j}
  → G ≃ᴳ H → is-trivialᴳ G → is-trivialᴳ H
iso-preserves-trivial iso G-is-trivial h =
    ! (GroupIso.f-g iso h)
  ∙ ap (GroupIso.f iso) (G-is-trivial _)
  ∙ GroupIso.pres-ident iso

iso-preserves'-trivial : ∀ {i j} {G : Group i} {H : Group j}
  → G ≃ᴳ H → is-trivialᴳ H → is-trivialᴳ G
iso-preserves'-trivial iso H-is-trivial g =
    ! (GroupIso.g-f iso g)
  ∙ ap (GroupIso.g iso) (H-is-trivial _)
  ∙ GroupHom.pres-ident (GroupIso.g-hom iso)

-- a surjective and injective homomorphism is an isomorphism
module _ {i j} {G : Group i} {H : Group j} (φ : G →ᴳ H)
  (surj : is-surjᴳ φ) (inj : is-injᴳ φ) where
  private
    module G = Group G
    module H = Group H
    module φ = GroupHom φ

    abstract
      image-prop : (h : H.El) → is-prop (hfiber φ.f h)
      image-prop h = all-paths-is-prop λ {(g₁ , p₁) (g₂ , p₂) →
          pair= (inj g₁ g₂ (p₁ ∙ ! p₂)) prop-has-all-paths-↓}
    instance
      image-prop-instance : {h : H.El} → is-prop (hfiber φ.f h)
      image-prop-instance = image-prop _

  surjᴳ-and-injᴳ-is-equiv : is-equiv φ.f
  surjᴳ-and-injᴳ-is-equiv = contr-map-is-equiv
    (λ h → let (g₁ , p₁) = Trunc-rec (idf _) (surj h) in
      has-level-in ((g₁ , p₁) , (λ {(g₂ , p₂) →
        pair= (inj g₁ g₂ (p₁ ∙ ! p₂))
                prop-has-all-paths-↓})))

  surjᴳ-and-injᴳ-iso : G ≃ᴳ H
  surjᴳ-and-injᴳ-iso = φ , surjᴳ-and-injᴳ-is-equiv


-- isomorphisms preserve abelianess.
module _ {i} {G H : Group i} (iso : G ≃ᴳ H) (G-abelian : is-abelian G) where
  private
    module G = Group G
    module H = Group H
    open GroupIso iso

  abstract
    iso-preserves-abelian : is-abelian H
    iso-preserves-abelian h₁ h₂ =
      H.comp h₁ h₂
        =⟨ ap2 H.comp (! $ f-g h₁) (! $ f-g h₂) ⟩
      H.comp (f (g h₁)) (f (g h₂))
        =⟨ ! $ pres-comp (g h₁) (g h₂) ⟩
      f (G.comp (g h₁) (g h₂))
        =⟨ G-abelian (g h₁) (g h₂) |in-ctx f ⟩
      f (G.comp (g h₂) (g h₁))
        =⟨ pres-comp (g h₂) (g h₁) ⟩
      H.comp (f (g h₂)) (f (g h₁))
        =⟨ ap2 H.comp (f-g h₂) (f-g h₁) ⟩
      H.comp h₂ h₁
        =∎

pre∘ᴳ-iso : ∀ {i j k} {G : Group i} {H : Group j} (K : AbGroup k)
  → (G ≃ᴳ H) → (hom-group H K ≃ᴳ hom-group G K)
pre∘ᴳ-iso K iso = ≃-to-≃ᴳ (equiv to from to-from from-to) to-pres-comp where
  to = GroupHom.f (pre∘ᴳ-hom K (–>ᴳ iso))
  to-pres-comp = GroupHom.pres-comp (pre∘ᴳ-hom K (–>ᴳ iso))
  from = GroupHom.f (pre∘ᴳ-hom K (<–ᴳ iso))
  abstract
    to-from : ∀ φ → to (from φ) == φ
    to-from φ = group-hom= $ λ= λ g → ap (GroupHom.f φ) (GroupIso.g-f iso g)

    from-to : ∀ φ → from (to φ) == φ
    from-to φ = group-hom= $ λ= λ h → ap (GroupHom.f φ) (GroupIso.f-g iso h)

post∘ᴳ-iso : ∀ {i j k} (G : Group i) (H : AbGroup j) (K : AbGroup k)
  → (AbGroup.grp H ≃ᴳ AbGroup.grp K) → (hom-group G H ≃ᴳ hom-group G K)
post∘ᴳ-iso G H K iso = ≃-to-≃ᴳ (equiv to from to-from from-to) to-pres-comp where
  to = GroupHom.f (post∘ᴳ-hom G H K (–>ᴳ iso))
  to-pres-comp = GroupHom.pres-comp (post∘ᴳ-hom G H K(–>ᴳ iso))
  from = GroupHom.f (post∘ᴳ-hom G K H (<–ᴳ iso))
  abstract
    to-from : ∀ φ → to (from φ) == φ
    to-from φ = group-hom= $ λ= λ g → GroupIso.f-g iso (GroupHom.f φ g)

    from-to : ∀ φ → from (to φ) == φ
    from-to φ = group-hom= $ λ= λ h → GroupIso.g-f iso (GroupHom.f φ h)

-- SIP for groups

module _ {i} (G₁ : Group i) where

  open Group G₁

  -- big nested Σ-type to be contracted
  private
    θ =
      [ ((El₂ , _) , ( map , _ ) ) ∈ Σ (0 -Type i) (λ ( El₂ , _ ) → El ≃ El₂) ] ×
       [ (mu₂ , _) ∈ Σ (El₂ → El₂ → El₂) (λ mu₂ → (x y : El) → map (comp x y) == mu₂ (map x) (map y)) ] ×
         [ (id₂ , _) ∈ Σ El₂ (λ id₂ → map ident == id₂) ] ×
           [ ( inv₂ , _ ) ∈ Σ (El₂ → El₂) (λ inv₂ → (x : El) → map (inv x) == inv₂ (map x)) ] ×
             ((x : El₂) → mu₂ id₂ x == x) × ((x y z : El₂) → mu₂ (mu₂ x y) z == mu₂ x (mu₂ y z)) × ((x : El₂) → mu₂ (inv₂ x) x == id₂)
                
  abstract

    grpiso-contr-aux : θ ≃ Unit
    grpiso-contr-aux =
      θ
        ≃⟨ Σ-contr-red (nType=-contr (El , ⟨⟩)) ⟩
      [ (mu₂ , _) ∈ Σ (El → El → El) (λ mu₂ → (x y : El) → comp x y == mu₂ x y) ] ×
         [ ( id₂ , _ ) ∈ Σ El (λ id₂ → ident == id₂) ] ×
           [ ( inv₂ , _ ) ∈ Σ (El → El) (λ inv₂ → (x : El) → inv x == inv₂ x) ] ×
             ((x : El) → mu₂ id₂ x == x) × ((x y z : El) → mu₂ (mu₂ x y) z == mu₂ x (mu₂ y z)) × ((x : El) → mu₂ (inv₂ x) x == id₂)
        ≃⟨ Σ-contr-red (funhom-iter-contr (S I) comp) ⟩
      [ ( id₂ , _ ) ∈ Σ El (λ id₂ → ident == id₂) ] ×
        [ ( inv₂ , _ ) ∈ Σ (El → El) (λ inv₂ → (x : El) → inv x == inv₂ x) ] ×
           ((x : El) → comp id₂ x == x) × ((x y z : El) → comp (comp x y) z == comp x (comp y z)) × ((x : El) → comp (inv₂ x) x == id₂)
        ≃⟨ Σ-contr-red (pathfrom-is-contr ident) ⟩
      [ ( inv₂ , _ ) ∈ Σ (El → El) (λ inv₂ → (x : El) → inv x == inv₂ x) ] ×
        ((x : El) → comp ident x == x) × ((x y z : El) → comp (comp x y) z == comp x (comp y z)) × ((x : El) → comp (inv₂ x) x == ident)
        ≃⟨ Σ-contr-red funhom-contr ⟩
      ((x : El) → comp ident x == x) × ((x y z : El) → comp (comp x y) z == comp x (comp y z)) × ((x : El) → comp (inv x) x == ident)
        ≃⟨ contr-equiv-Unit (inhab-prop-is-contr (unit-l , assoc , inv-l)) ⟩
      Unit ≃∎

    grpisof-Σ-≃ : Σ (Group i) (λ G₂ → G₁ ≃ᴳ G₂) ≃ θ
    grpisof-Σ-≃ = let
      open GroupStructure
      open GroupHom in
      equiv
        (λ ((group El₂ {{El₂-level}} σ) , iso@(h , _)) →
          ((El₂ , El₂-level) , GroupIso.f-equiv iso) ,
          (comp σ , pres-comp h) ,
          ((ident σ) , (pres-ident h)) ,
          (((inv σ) , (pres-inv h)) ,
          (unit-l σ) , (assoc σ) , (inv-l σ)))
        (λ (((El₂ , El₂-level) , (h , eqv)) , (comp₂ , pres-comp₂) , (id₂ , _) , ((inv₂ , _) , unit-l₂ , assoc₂ , inv-l₂))
          → group El₂ {{El₂-level}} (group-structure id₂ inv₂ comp₂ unit-l₂ assoc₂ inv-l₂) , (group-hom h pres-comp₂) , eqv)
        (λ (((El₂ , El₂-level) , (h , eqv)) , (comp₂ , pres-comp₂) , (id₂ , _) , ((inv₂ , _) , unit-l₂ , assoc₂ , inv-l₂)) →
          ap2 (λ p₁ p₂ →  (((El₂ , El₂-level) , (h , eqv)) , (comp₂ , pres-comp₂) , (id₂ , p₁) , ((inv₂ , p₂) , unit-l₂ , assoc₂ , inv-l₂)))
            (prop-has-all-paths {{has-level-apply-instance {{El₂-level}}}} _ _)
            (prop-has-all-paths {{Π-level λ _ → has-level-apply-instance {{El₂-level}}}} _ _))
        λ _ → idp

  grpiso-contr : is-contr (Σ (Group i) (λ G₂ → G₁ ≃ᴳ G₂))
  grpiso-contr = equiv-preserves-level ((grpiso-contr-aux ∘e grpisof-Σ-≃) ⁻¹)

module _ {i} {G₁ : Group i} where

  grpiso-ind : ∀ {k} (P : (G₂ : Group i) → G₁ ≃ᴳ G₂ → Type k)
    → P G₁ (idiso G₁) → {G₂ : Group i} (m : G₁ ≃ᴳ G₂) → P G₂ m
  grpiso-ind P = ID-ind-map P (grpiso-contr G₁)

  grpiso-ind-β : ∀ {k} (P : (G₂ : Group i) → (G₁ ≃ᴳ G₂ → Type k))
    → (r : P G₁ (idiso G₁)) → grpiso-ind P r (idiso G₁) == r
  grpiso-ind-β P = ID-ind-map-β P (grpiso-contr G₁)
  
  grpiso-to-== : {G₂ : Group i} → G₁ ≃ᴳ G₂ → G₁ == G₂
  grpiso-to-== = grpiso-ind (λ G₂ _ → G₁ == G₂) idp

  abstract
    grpiso-to-==-β : grpiso-to-== (idiso G₁) == idp
    grpiso-to-==-β = grpiso-ind-β (λ G₂ _ → G₁ == G₂) idp

  grpiso-from-== : {G₂ : Group i} → G₁ == G₂ → G₁ ≃ᴳ G₂
  grpiso-from-== idp = idiso G₁

  univᴳ : {G₂ : Group i} → (G₁ ≃ᴳ G₂) ≃ (G₁ == G₂)
  univᴳ = equiv grpiso-to-== grpiso-from-== rt1 rt2
    where

      rt1 : ∀ {G₂} (p : G₁ == G₂) → grpiso-to-== (grpiso-from-== p) == p
      rt1 idp = grpiso-to-==-β

      rt2 : ∀ {G₂} (p : G₁ ≃ᴳ G₂) → grpiso-from-== (grpiso-to-== p) == p
      rt2 = grpiso-ind (λ _ p → grpiso-from-== (grpiso-to-== p) == p) (ap grpiso-from-== grpiso-to-==-β)

instance

  Grp-isGrpd : ∀ {i} → has-level 1 (Group i)
  Grp-isGrpd = has-level-in (λ G₁ G₂ → equiv-preserves-level univᴳ)

  AbGrp-isGrpd : ∀ {i} → has-level 1 (AbGroup i)
  AbGrp-isGrpd = Subtype-level (subtypeprop is-abelian)