------------------------------------------------------------------------
-- Groups
------------------------------------------------------------------------

{-# OPTIONS --cubical-compatible --safe #-}

open import Equality

module Group
  {e⁺} (eq : ∀ {a p} → Equality-with-J a p e⁺) where

open Derived-definitions-and-properties eq

open import Logical-equivalence using (_⇔_)
open import Prelude as P hiding (id; _∘_) renaming (_×_ to _⊗_)

import Bijection eq as B
open import Equivalence eq as Eq using (_≃_)
open import Extensionality eq
open import Function-universe eq as F hiding (id; _∘_)
open import Groupoid eq using (Groupoid)
open import H-level eq
open import H-level.Closure eq
open import Integer.Basics eq using (+_; -[1+_])
open import Univalence-axiom eq

private
  variable
    a g₁ g₂ : Level
    A       : Type a
    g x y   : A
    k       : Kind

------------------------------------------------------------------------
-- Groups

-- Groups.
--
-- Note that the carrier type is required to be a set (following the
-- HoTT book).

record Group g : Type (lsuc g) where
  infix   _⁻¹
  infixr  _∘_

  field
    Carrier        : Type g
    Carrier-is-set : Is-set Carrier
    _∘_            : Carrier → Carrier → Carrier
    id             : Carrier
    _⁻¹            : Carrier → Carrier
    left-identity  : ∀ x → (id ∘ x) ≡ x
    right-identity : ∀ x → (x ∘ id) ≡ x
    assoc          : ∀ x y z → (x ∘ (y ∘ z)) ≡ ((x ∘ y) ∘ z)
    left-inverse   : ∀ x → ((x ⁻¹) ∘ x) ≡ id
    right-inverse  : ∀ x → (x ∘ (x ⁻¹)) ≡ id

  -- Groups are groupoids.

  groupoid : Groupoid lzero g
  groupoid = record
    { Object         = ⊤
    ; _∼_            = λ _ _ → Carrier
    ; id             = id
    ; _∘_            = _∘_
    ; _⁻¹            = _⁻¹
    ; left-identity  = left-identity
    ; right-identity = right-identity
    ; assoc          = assoc
    ; left-inverse   = left-inverse
    ; right-inverse  = right-inverse
    }

  open Groupoid groupoid public
    hiding (Object; _∼_; id; _∘_; _⁻¹; left-identity; right-identity;
            assoc; left-inverse; right-inverse)

private
  variable
    G G₁ G₁′ G₂ G₂′ G₃ : Group g

-- The type of groups can be expressed using a nested Σ-type.

Group-as-Σ :
  Group g ≃
  ∃ λ (A : Set g) →
  let A = ⌞ A ⌟ in
  ∃ λ (_∘_ : A → A → A) →
  ∃ λ (id : A) →
  ∃ λ (_⁻¹ : A → A) →
    (∀ x → (id ∘ x) ≡ x) ⊗
    (∀ x → (x ∘ id) ≡ x) ⊗
    (∀ x y z → (x ∘ (y ∘ z)) ≡ ((x ∘ y) ∘ z)) ⊗
    (∀ x → ((x ⁻¹) ∘ x) ≡ id) ⊗
    (∀ x → (x ∘ (x ⁻¹)) ≡ id)
Group-as-Σ =
  Eq.↔→≃
    (λ G → let open Group G in
         (Carrier , Carrier-is-set)
       , _∘_
       , id
       , _⁻¹
       , left-identity
       , right-identity
       , assoc
       , left-inverse
       , right-inverse)
    _
    refl
    refl

------------------------------------------------------------------------
-- Group homomorphisms and isomorphisms

-- Group homomorphisms (generalised to several kinds of underlying
-- "functions").

record Homomorphic (k : Kind) (G₁ : Group g₁) (G₂ : Group g₂) :
                   Type (g₁ ⊔ g₂) where
  private
    module G₁ = Group G₁
    module G₂ = Group G₂

  field
    related : G₁.Carrier ↝[ k ] G₂.Carrier

  to : G₁.Carrier → G₂.Carrier
  to = to-implication related

  field
    homomorphic :
      ∀ x y → to (x G₁.∘ y) ≡ to x G₂.∘ to y

open Homomorphic public using (related; homomorphic)
open Homomorphic using (to)

-- The type of (generalised) group homomorphisms can be expressed
-- using a nested Σ-type.

Homomorphic-as-Σ :
  {G₁ : Group g₁} {G₂ : Group g₂} →
  Homomorphic k G₁ G₂ ≃
  let module G₁ = Group G₁
      module G₂ = Group G₂
  in
  ∃ λ (f : G₁.Carrier ↝[ k ] G₂.Carrier) →
    ∀ x y →
    to-implication f (x G₁.∘ y) ≡
    to-implication f x G₂.∘ to-implication f y
Homomorphic-as-Σ =
  Eq.↔→≃
    (λ G₁↝G₂ → G₁↝G₂ .related , G₁↝G₂ .homomorphic)
    _
    refl
    refl

-- A variant of Homomorphic.

infix  _↝[_]ᴳ_ _→ᴳ_ _≃ᴳ_

_↝[_]ᴳ_ : Group g₁ → Kind → Group g₂ → Type (g₁ ⊔ g₂)
_↝[_]ᴳ_ = flip Homomorphic

-- Group homomorphisms.

_→ᴳ_ : Group g₁ → Group g₂ → Type (g₁ ⊔ g₂)
_→ᴳ_ = _↝[ implication ]ᴳ_

-- Group isomorphisms.

_≃ᴳ_ : Group g₁ → Group g₂ → Type (g₁ ⊔ g₂)
_≃ᴳ_ = _↝[ equivalence ]ᴳ_

-- "Functions" of type G₁ ↝[ k ]ᴳ G₂ can be converted to group
-- homomorphisms.

↝ᴳ→→ᴳ : G₁ ↝[ k ]ᴳ G₂ → G₁ →ᴳ G₂
↝ᴳ→→ᴳ f .related     = to f
↝ᴳ→→ᴳ f .homomorphic = f .homomorphic

-- _↝[ k ]ᴳ_ is reflexive.

↝ᴳ-refl : G ↝[ k ]ᴳ G
↝ᴳ-refl         .related         = F.id
↝ᴳ-refl {G} {k} .homomorphic x y =
  to-implication {k = k} F.id (x ∘ y)  ≡⟨ cong (_$ _) $ to-implication-id k ⟩

  x ∘ y                                ≡⟨ sym $ cong₂ (λ f g → f _ ∘ g _)
                                            (to-implication-id k)
                                            (to-implication-id k) ⟩∎
  to-implication {k = k} F.id x ∘
  to-implication {k = k} F.id y        ∎
  where
  open Group G

-- _↝[ k ]ᴳ_ is transitive.

↝ᴳ-trans : G₁ ↝[ k ]ᴳ G₂ → G₂ ↝[ k ]ᴳ G₃ → G₁ ↝[ k ]ᴳ G₃
↝ᴳ-trans {G₁} {k} {G₂} {G₃} G₁↝G₂ G₂↝G₃ = λ where
    .related         → G₂↝G₃ .related F.∘ G₁↝G₂ .related
    .homomorphic x y →
      to-implication (G₂↝G₃ .related F.∘ G₁↝G₂ .related) (x G₁.∘ y)  ≡⟨ cong (_$ _) $ to-implication-∘ k ⟩

      to G₂↝G₃ (to G₁↝G₂ (x G₁.∘ y))                                 ≡⟨ cong (to G₂↝G₃) $ homomorphic G₁↝G₂ _ _ ⟩

      to G₂↝G₃ (to G₁↝G₂ x G₂.∘ to G₁↝G₂ y)                          ≡⟨ homomorphic G₂↝G₃ _ _ ⟩

      to G₂↝G₃ (to G₁↝G₂ x) G₃.∘ to G₂↝G₃ (to G₁↝G₂ y)               ≡⟨ sym $ cong₂ (λ f g → f _ G₃.∘ g _)
                                                                          (to-implication-∘ k)
                                                                          (to-implication-∘ k) ⟩∎
      to-implication (G₂↝G₃ .related F.∘ G₁↝G₂ .related) x G₃.∘
      to-implication (G₂↝G₃ .related F.∘ G₁↝G₂ .related) y           ∎
  where
  module G₁ = Group G₁
  module G₂ = Group G₂
  module G₃ = Group G₃

-- _≃ᴳ_ is symmetric.

≃ᴳ-sym : G₁ ≃ᴳ G₂ → G₂ ≃ᴳ G₁
≃ᴳ-sym {G₁} {G₂} G₁≃G₂ = λ where
    .related         → inverse (G₁≃G₂ .related)
    .homomorphic x y → _≃_.injective (G₁≃G₂ .related)
      (to G₁≃G₂ (_≃_.from (G₁≃G₂ .related) (x G₂.∘ y))                   ≡⟨ _≃_.right-inverse-of (G₁≃G₂ .related) _ ⟩

       x G₂.∘ y                                                          ≡⟨ sym $ cong₂ G₂._∘_
                                                                              (_≃_.right-inverse-of (G₁≃G₂ .related) _)
                                                                              (_≃_.right-inverse-of (G₁≃G₂ .related) _) ⟩
       to G₁≃G₂ (_≃_.from (G₁≃G₂ .related) x) G₂.∘
       to G₁≃G₂ (_≃_.from (G₁≃G₂ .related) y)                            ≡⟨ sym $ G₁≃G₂ .homomorphic _ _ ⟩∎

       to G₁≃G₂
         (_≃_.from (G₁≃G₂ .related) x G₁.∘ _≃_.from (G₁≃G₂ .related) y)  ∎)
  where
  module G₁ = Group G₁
  module G₂ = Group G₂

-- Group homomorphisms preserve identity elements.

→ᴳ-id :
  (G₁↝G₂ : G₁ ↝[ k ]ᴳ G₂) →
  to G₁↝G₂ (Group.id G₁) ≡ Group.id G₂
→ᴳ-id {G₁} {G₂} G₁↝G₂ =
  G₂.idempotent⇒≡id
    (to G₁↝G₂ G₁.id G₂.∘ to G₁↝G₂ G₁.id  ≡⟨ sym $ G₁↝G₂ .homomorphic _ _ ⟩
     to G₁↝G₂ (G₁.id G₁.∘ G₁.id)         ≡⟨ cong (to G₁↝G₂) $ G₁.left-identity _ ⟩∎
     to G₁↝G₂ G₁.id                      ∎)
  where
  module G₁ = Group G₁
  module G₂ = Group G₂

-- Group homomorphisms are homomorphic with respect to the inverse
-- operators.

→ᴳ-⁻¹ :
  ∀ (G₁↝G₂ : G₁ ↝[ k ]ᴳ G₂) x →
  to G₁↝G₂ (Group._⁻¹ G₁ x) ≡ Group._⁻¹ G₂ (to G₁↝G₂ x)
→ᴳ-⁻¹ {G₁} {G₂} G₁↝G₂ x = G₂.⁻¹∘≡id→≡
  (to G₁↝G₂ x G₂.⁻¹ G₂.⁻¹ G₂.∘ to G₁↝G₂ (x G₁.⁻¹)  ≡⟨ cong (G₂._∘ to G₁↝G₂ (x G₁.⁻¹)) $ G₂.involutive _ ⟩
   to G₁↝G₂ x G₂.∘ to G₁↝G₂ (x G₁.⁻¹)              ≡⟨ sym $ G₁↝G₂ .homomorphic _ _ ⟩
   to G₁↝G₂ (x G₁.∘ x G₁.⁻¹)                       ≡⟨ cong (to G₁↝G₂) (G₁.right-inverse _) ⟩
   to G₁↝G₂ G₁.id                                  ≡⟨ →ᴳ-id G₁↝G₂ ⟩∎
   G₂.id                                           ∎)
  where
  module G₁ = Group G₁
  module G₂ = Group G₂

-- Group homomorphisms are homomorphic with respect to exponentiation.

→ᴳ-^ :
  ∀ (G₁↝G₂ : G₁ ↝[ k ]ᴳ G₂) x i →
  to G₁↝G₂ (Group._^_ G₁ x i) ≡
  Group._^_ G₂ (to G₁↝G₂ x) i
→ᴳ-^ {G₁} {G₂} G₁↝G₂ x = lemma₂
  where
  module G₁ = Group G₁
  module G₂ = Group G₂

  lemma₁ : ∀ n → to G₁↝G₂ (y G₁.^+ n) ≡ to G₁↝G₂ y G₂.^+ n
  lemma₁ zero =
    to G₁↝G₂ G₁.id  ≡⟨ →ᴳ-id G₁↝G₂ ⟩∎
    G₂.id    ∎
  lemma₁ {y} (suc n) =
    to G₁↝G₂ (y G₁.∘ y G₁.^+ n)           ≡⟨ G₁↝G₂ .homomorphic _ _ ⟩
    to G₁↝G₂ y G₂.∘ to G₁↝G₂ (y G₁.^+ n)  ≡⟨ cong (_ G₂.∘_) $ lemma₁ n ⟩∎
    to G₁↝G₂ y G₂.∘ to G₁↝G₂ y G₂.^+ n    ∎

  lemma₂ : ∀ i → to G₁↝G₂ (x G₁.^ i) ≡ to G₁↝G₂ x G₂.^ i
  lemma₂ (+ n)    = lemma₁ n
  lemma₂ -[1+ n ] =
    to G₁↝G₂ ((x G₁.⁻¹) G₁.^+ suc n)  ≡⟨ lemma₁ (suc n) ⟩
    to G₁↝G₂ (x G₁.⁻¹) G₂.^+ suc n    ≡⟨ cong (G₂._^+ suc n) $ →ᴳ-⁻¹ G₁↝G₂ _ ⟩∎
    (to G₁↝G₂ x G₂.⁻¹) G₂.^+ suc n    ∎

-- Group equality can be expressed in terms of equality of pairs of
-- carrier types and binary operators (assuming extensionality).

≡≃,∘≡,∘ :
  {G₁ G₂ : Group g} →
  Extensionality g g →
  let module G₁ = Group G₁
      module G₂ = Group G₂
  in
  (G₁ ≡ G₂) ≃ ((G₁.Carrier , G₁._∘_) ≡ (G₂.Carrier , G₂._∘_))
≡≃,∘≡,∘ {g} {G₁} {G₂} ext =
  G₁ ≡ G₂                                                    ↝⟨ inverse $ Eq.≃-≡ Group≃ ⟩

  ((G₁.Carrier , G₁._∘_) , _) ≡ ((G₂.Carrier , G₂._∘_) , _)  ↔⟨ (inverse $
                                                                 ignore-propositional-component $
                                                                 The-rest-propositional _) ⟩□
  (G₁.Carrier , G₁._∘_) ≡ (G₂.Carrier , G₂._∘_)              □
  where
  module G₁ = Group G₁
  module G₂ = Group G₂

  Carrier-∘ = ∃ λ (C : Type g) → (C → C → C)

  The-rest : Carrier-∘ → Type g
  The-rest (C , _∘_) =
    ∃ λ ((id , _⁻¹) : C ⊗ (C → C)) →
      Is-set C ⊗
      (∀ x → (id ∘ x) ≡ x) ⊗
      (∀ x → (x ∘ id) ≡ x) ⊗
      (∀ x y z → (x ∘ (y ∘ z)) ≡ ((x ∘ y) ∘ z)) ⊗
      (∀ x → ((x ⁻¹) ∘ x) ≡ id) ⊗
      (∀ x → (x ∘ (x ⁻¹)) ≡ id)

  Group≃ : Group g ≃ Σ Carrier-∘ The-rest
  Group≃ = Eq.↔→≃
    (λ G → let open Group G in
         (Carrier , _∘_)
       , (id , _⁻¹)
       , Carrier-is-set , left-identity , right-identity , assoc
       , left-inverse , right-inverse)
    _
    refl
    refl

  The-rest-propositional : ∀ C → Is-proposition (The-rest C)
  The-rest-propositional C R₁ R₂ =
    Σ-≡,≡→≡
      (cong₂ _,_ id-unique inverse-unique)
      ((×-closure  (H-level-propositional ext ) $
        ×-closure  (Π-closure ext  λ _ →
                     G₂′.Carrier-is-set) $
        ×-closure  (Π-closure ext  λ _ →
                     G₂′.Carrier-is-set) $
        ×-closure  (Π-closure ext  λ _ →
                     Π-closure ext  λ _ →
                     Π-closure ext  λ _ →
                     G₂′.Carrier-is-set) $
        ×-closure  (Π-closure ext  λ _ →
                     G₂′.Carrier-is-set) $
                    (Π-closure ext  λ _ →
                     G₂′.Carrier-is-set))
         _ _)
    where
    module G₁′ = Group (_≃_.from Group≃ (C , R₁))
    module G₂′ = Group (_≃_.from Group≃ (C , R₂))

    id-unique : G₁′.id ≡ G₂′.id
    id-unique = G₂′.idempotent⇒≡id (G₁′.left-identity G₁′.id)

    inverse-unique : G₁′._⁻¹ ≡ G₂′._⁻¹
    inverse-unique = apply-ext ext λ x → G₂′.⁻¹-unique-right
      (x G₁′.∘ x G₁′.⁻¹  ≡⟨ G₁′.right-inverse _ ⟩
       G₁′.id            ≡⟨ id-unique ⟩∎
       G₂′.id            ∎)

-- Group isomorphisms are equivalent to equalities (assuming
-- extensionality and univalence).

≃ᴳ≃≡ :
  {G₁ G₂ : Group g} →
  Extensionality g g →
  Univalence g →
  (G₁ ≃ᴳ G₂) ≃ (G₁ ≡ G₂)
≃ᴳ≃≡ {G₁} {G₂} ext univ =
  G₁ ≃ᴳ G₂                                                              ↝⟨ Homomorphic-as-Σ ⟩

  (∃ λ (eq : G₁.Carrier ≃ G₂.Carrier) →
     ∀ x y →
     _≃_.to eq (x G₁.∘ y) ≡ _≃_.to eq x G₂.∘ _≃_.to eq y)               ↝⟨ (∃-cong λ eq → Π-cong ext eq λ _ → Π-cong ext eq λ _ →
                                                                            ≡⇒≃ $ sym $ cong (_≡ _≃_.to eq _ G₂.∘ _≃_.to eq _) $ cong (_≃_.to eq) $
                                                                            cong₂ G₁._∘_
                                                                              (_≃_.left-inverse-of eq _)
                                                                              (_≃_.left-inverse-of eq _)) ⟩
  (∃ λ (eq : G₁.Carrier ≃ G₂.Carrier) →
     ∀ x y → _≃_.to eq (_≃_.from eq x G₁.∘ _≃_.from eq y) ≡ x G₂.∘ y)   ↝⟨ (∃-cong λ _ → ∀-cong ext λ _ →
                                                                            Eq.extensionality-isomorphism ext) ⟩
  (∃ λ (eq : G₁.Carrier ≃ G₂.Carrier) →
     ∀ x →
     (λ y → _≃_.to eq (_≃_.from eq x G₁.∘ _≃_.from eq y)) ≡ (x G₂.∘_))  ↝⟨ (∃-cong λ _ →
                                                                            Eq.extensionality-isomorphism ext) ⟩
  (∃ λ (eq : G₁.Carrier ≃ G₂.Carrier) →
     (λ x y → _≃_.to eq (_≃_.from eq x G₁.∘ _≃_.from eq y)) ≡ G₂._∘_)   ↝⟨ (∃-cong λ eq → ≡⇒≃ $ cong (_≡ _) $ sym $ lemma eq) ⟩

  (∃ λ (eq : G₁.Carrier ≃ G₂.Carrier) →
     subst (λ A → A → A → A) (≃⇒≡ univ eq) G₁._∘_ ≡ G₂._∘_)             ↝⟨ (Σ-cong (inverse $ ≡≃≃ univ) λ _ → Eq.id) ⟩

  (∃ λ (eq : G₁.Carrier ≡ G₂.Carrier) →
     subst (λ A → A → A → A) eq G₁._∘_ ≡ G₂._∘_)                        ↔⟨ B.Σ-≡,≡↔≡ ⟩

  ((G₁.Carrier , G₁._∘_) ≡ (G₂.Carrier , G₂._∘_))                       ↝⟨ inverse $ ≡≃,∘≡,∘ ext ⟩□

  G₁ ≡ G₂                                                               □
  where
  module G₁ = Group G₁
  module G₂ = Group G₂

  lemma : ∀ _ → _
  lemma = λ eq → apply-ext ext λ x → apply-ext ext λ y →
    subst (λ A → A → A → A) (≃⇒≡ univ eq) G₁._∘_ x y      ≡⟨ cong (_$ y) subst-→ ⟩

    subst (λ A → A → A) (≃⇒≡ univ eq)
      (subst P.id (sym (≃⇒≡ univ eq)) x G₁.∘_) y          ≡⟨ subst-→ ⟩

    subst P.id (≃⇒≡ univ eq)
      (subst P.id (sym (≃⇒≡ univ eq)) x G₁.∘
       subst P.id (sym (≃⇒≡ univ eq)) y)                  ≡⟨ cong₂ (λ f g → f (g x G₁.∘ g y))
                                                               (trans (apply-ext ext λ _ → subst-id-in-terms-of-≡⇒↝ equivalence) $
                                                                cong _≃_.to $ _≃_.right-inverse-of (≡≃≃ univ) _)
                                                               (trans (apply-ext ext λ _ → subst-id-in-terms-of-inverse∘≡⇒↝ equivalence) $
                                                                cong _≃_.from $ _≃_.right-inverse-of (≡≃≃ univ) _) ⟩∎
    _≃_.to eq (_≃_.from eq x G₁.∘ _≃_.from eq y)          ∎

------------------------------------------------------------------------
-- Abelian groups

-- The property of being abelian.

Abelian : Group g → Type g
Abelian G =
  ∀ x y → x ∘ y ≡ y ∘ x
  where
  open Group G

-- If two groups are isomorphic, and one is abelian, then the other
-- one is abelian.

≃ᴳ→Abelian→Abelian : G₁ ≃ᴳ G₂ → Abelian G₁ → Abelian G₂
≃ᴳ→Abelian→Abelian {G₁} {G₂} G₁≃G₂ ∘-comm x y =
  _≃_.injective (G₂≃G₁ .related)
    (to G₂≃G₁ (x G₂.∘ y)         ≡⟨ G₂≃G₁ .homomorphic _ _ ⟩
     to G₂≃G₁ x G₁.∘ to G₂≃G₁ y  ≡⟨ ∘-comm _ _ ⟩
     to G₂≃G₁ y G₁.∘ to G₂≃G₁ x  ≡⟨ sym $ G₂≃G₁ .homomorphic _ _ ⟩∎
     to G₂≃G₁ (y G₂.∘ x)         ∎)
  where
  module G₁ = Group G₁
  module G₂ = Group G₂

  G₂≃G₁ = ≃ᴳ-sym G₁≃G₂

------------------------------------------------------------------------
-- A group construction

-- The direct product of two groups.

infixr  _×_

_×_ : Group g₁ → Group g₂ → Group (g₁ ⊔ g₂)
G₁ × G₂ = λ where
    .Carrier          → G₁.Carrier ⊗ G₂.Carrier
    .Carrier-is-set   → ×-closure  G₁.Carrier-is-set G₂.Carrier-is-set
    ._∘_              → Σ-zip G₁._∘_ G₂._∘_
    .id               → G₁.id , G₂.id
    ._⁻¹              → Σ-map G₁._⁻¹ G₂._⁻¹
    .left-identity _  → cong₂ _,_
                          (G₁.left-identity _) (G₂.left-identity _)
    .right-identity _ → cong₂ _,_
                          (G₁.right-identity _) (G₂.right-identity _)
    .assoc _ _ _      → cong₂ _,_ (G₁.assoc _ _ _) (G₂.assoc _ _ _)
    .left-inverse _   → cong₂ _,_
                          (G₁.left-inverse _) (G₂.left-inverse _)
    .right-inverse _  → cong₂ _,_
                          (G₁.right-inverse _) (G₂.right-inverse _)
  where
  open Group

  module G₁ = Group G₁
  module G₂ = Group G₂

-- The direct product operator preserves group homomorphisms.

↝-× :
  G₁ ↝[ k ]ᴳ G₂ → G₁′ ↝[ k ]ᴳ G₂′ →
  (G₁ × G₁′) ↝[ k ]ᴳ (G₂ × G₂′)
↝-× {G₁} {k} {G₂} {G₁′} {G₂′} G₁↝G₂ G₁′↝G₂′ = λ where
  .related →
    G₁↝G₂ .related ×-cong G₁′↝G₂′ .related
  .homomorphic x@(x₁ , x₂) y@(y₁ , y₂) →
    to-implication (G₁↝G₂ .related ×-cong G₁′↝G₂′ .related)
      (Σ-zip (Group._∘_ G₁) (Group._∘_ G₁′) x y)                   ≡⟨ cong (_$ _) $ to-implication-×-cong k ⟩

    Σ-map (to G₁↝G₂) (to G₁′↝G₂′)
      (Σ-zip (Group._∘_ G₁) (Group._∘_ G₁′) x y)                   ≡⟨⟩

    to G₁↝G₂   (Group._∘_ G₁  x₁ y₁) ,
    to G₁′↝G₂′ (Group._∘_ G₁′ x₂ y₂)                               ≡⟨ cong₂ _,_
                                                                        (G₁↝G₂   .homomorphic _ _)
                                                                        (G₁′↝G₂′ .homomorphic _ _) ⟩
    Group._∘_ G₂  (to G₁↝G₂   x₁) (to G₁↝G₂   y₁) ,
    Group._∘_ G₂′ (to G₁′↝G₂′ x₂) (to G₁′↝G₂′ y₂)                  ≡⟨⟩

    Group._∘_ (G₂ × G₂′)
      (to G₁↝G₂ x₁ , to G₁′↝G₂′ x₂)
      (to G₁↝G₂ y₁ , to G₁′↝G₂′ y₂)                                ≡⟨ sym $ cong₂ (λ f g → Group._∘_ (G₂ × G₂′) (f _) (g _))
                                                                        (to-implication-×-cong k)
                                                                        (to-implication-×-cong k) ⟩∎
    Group._∘_ (G₂ × G₂′)
      (to-implication (G₁↝G₂ .related ×-cong G₁′↝G₂′ .related) x)
      (to-implication (G₁↝G₂ .related ×-cong G₁′↝G₂′ .related) y)  ∎

-- Exponentiation for the direct product of G₁ and G₂ can be expressed
-- in terms of exponentiation for G₁ and exponentiation for G₂.

^-× :
  ∀ (G₁ : Group g₁) (G₂ : Group g₂) {x y} i →
  Group._^_ (G₁ × G₂) (x , y) i ≡
  (Group._^_ G₁ x i , Group._^_ G₂ y i)
^-× G₁ G₂ = helper
  where
  module G₁  = Group G₁
  module G₂  = Group G₂
  module G₁₂ = Group (G₁ × G₂)

  +-helper : ∀ n → (x , y) G₁₂.^+ n ≡ (x G₁.^+ n , y G₂.^+ n)
  +-helper         zero    = refl _
  +-helper {x} {y} (suc n) =
    (x , y) G₁₂.∘ (x , y) G₁₂.^+ n         ≡⟨ cong (_ G₁₂.∘_) $ +-helper n ⟩
    (x , y) G₁₂.∘ (x G₁.^+ n , y G₂.^+ n)  ≡⟨⟩
    (x G₁.∘ x G₁.^+ n , y G₂.∘ y G₂.^+ n)  ∎

  helper : ∀ i → (x , y) G₁₂.^ i ≡ (x G₁.^ i , y G₂.^ i)
  helper (+ n)    = +-helper n
  helper -[1+ n ] = +-helper (suc n)

------------------------------------------------------------------------
-- The centre of a group

-- Centre ext G is the centre of the group G, sometimes denoted Z(G).

Centre :
  Extensionality g g →
  Group g → Group g
Centre ext G = λ where
    .Carrier        → ∃ λ (x : Carrier) → ∀ y → x ∘ y ≡ y ∘ x
    .Carrier-is-set → Σ-closure  Carrier-is-set λ _ →
                      Π-closure ext  λ _ →
                      mono₁  Carrier-is-set
    ._∘_            → Σ-zip _∘_ λ {x y} hyp₁ hyp₂ z →
                        (x ∘ y) ∘ z  ≡⟨ sym $ assoc _ _ _ ⟩
                        x ∘ (y ∘ z)  ≡⟨ cong (x ∘_) $ hyp₂ z ⟩
                        x ∘ (z ∘ y)  ≡⟨ assoc _ _ _ ⟩
                        (x ∘ z) ∘ y  ≡⟨ cong (_∘ y) $ hyp₁ z ⟩
                        (z ∘ x) ∘ y  ≡⟨ sym $ assoc _ _ _ ⟩∎
                        z ∘ (x ∘ y)  ∎
    .id             → id
                    , λ x →
                        id ∘ x  ≡⟨ left-identity _ ⟩
                        x       ≡⟨ sym $ right-identity _ ⟩∎
                        x ∘ id  ∎
    ._⁻¹            → Σ-map _⁻¹ λ {x} hyp y →
                        x ⁻¹ ∘ y        ≡⟨ cong (x ⁻¹ ∘_) $ sym $ involutive _ ⟩
                        x ⁻¹ ∘ y ⁻¹ ⁻¹  ≡⟨ sym ∘⁻¹ ⟩
                        (y ⁻¹ ∘ x) ⁻¹   ≡⟨ cong _⁻¹ $ sym $ hyp (y ⁻¹) ⟩
                        (x ∘ y ⁻¹) ⁻¹   ≡⟨ ∘⁻¹ ⟩
                        y ⁻¹ ⁻¹ ∘ x ⁻¹  ≡⟨ cong (_∘ x ⁻¹) $ involutive _ ⟩∎
                        y ∘ x ⁻¹        ∎
    .left-identity  → λ _ →
                      Σ-≡,≡→≡ (left-identity _)
                        ((Π-closure ext  λ _ → Carrier-is-set) _ _)
    .right-identity → λ _ →
                      Σ-≡,≡→≡ (right-identity _)
                        ((Π-closure ext  λ _ → Carrier-is-set) _ _)
    .assoc          → λ _ _ _ →
                      Σ-≡,≡→≡ (assoc _ _ _)
                        ((Π-closure ext  λ _ → Carrier-is-set) _ _)
    .left-inverse   → λ _ →
                      Σ-≡,≡→≡ (left-inverse _)
                        ((Π-closure ext  λ _ → Carrier-is-set) _ _)
    .right-inverse  → λ _ →
                      Σ-≡,≡→≡ (right-inverse _)
                        ((Π-closure ext  λ _ → Carrier-is-set) _ _)
  where
  open Group G

-- The centre of an abelian group is isomorphic to the group.

Abelian→Centre≃ :
  (ext : Extensionality g g) (G : Group g) →
  Abelian G → Centre ext G ≃ᴳ G
Abelian→Centre≃ ext G abelian = ≃ᴳ-sym λ where
    .Homomorphic.related         → inverse equiv
    .Homomorphic.homomorphic _ _ →
      cong (_ ,_) ((Π-closure ext  λ _ → Carrier-is-set) _ _)
  where
  open Group G

  equiv =
    (∃ λ (x : Carrier) → ∀ y → x ∘ y ≡ y ∘ x)  ↔⟨ (drop-⊤-right λ _ →
                                                   _⇔_.to contractible⇔↔⊤ $
                                                   Π-closure ext  λ _ →
                                                   propositional⇒inhabited⇒contractible
                                                     Carrier-is-set
                                                     (abelian _ _)) ⟩□
    Carrier                                    □