Classical.Structures.Group.Basic¶

Groups¶

This is the Classical.Structures.Group.Basic module of the Agda Universal Algebra Library.

A group is an inhabitant of the Σ[ 𝑨 ∈ Algebra α ρ ] 𝑨 ⊨ Th-Group type, where Algebra is parameterized by the signature type Sig-Group.

The signature of Group grows over its predecessor's by a unary symbol (Sig-Group adds ⁻¹-Op to Sig-Monoid); its forgetful projection group→monoid is therefore a reduct that drops ⁻¹-Op, discharging the three monoid equations on the reduct by the curried-law pivot of the monoid→semigroup of Classical.Structures.Monoid (here extended from one law to three, the two identity laws additionally bridging the nullary ε-Op node).

This module follows the Monoid template, adding the following to it.

Direct curried accessors for all three operations. Group-Op defines _∙_ = Curry₂ (∙-Op ^ 𝑨), ε = Curry₀ (ε-Op ^ 𝑨), and _⁻¹ = Curry₁ (⁻¹-Op ^ 𝑨) directly over Sig-Group, never inheriting through the reduct, for the same reason Monoid gives: keeping the accessors direct keeps every downstream refl off the reduct's position-map reduction.
A unary node-bridge. Alongside the binary interp-node-∙ and nullary interp-node-ε, Group-Op has interp-node-⁻¹ for the unary ⁻¹-Op, a one-liner delegating to interp-cong exactly as the other two do.
Two inverse laws. invˡ-law and invʳ-law join the three monoid laws in Group-Op; they are the only laws not consumed by the forgetful projection (which lands in Monoid, below the inverse structure), so they live in Group-Op rather than in the standalone curried-law block.

{-# OPTIONS --without-K --exact-split --safe #-}

module Classical.Structures.Group.Basic where

open import Agda.Primitive using () renaming ( Set to Type )

-- Imports from the Agda Standard Library -------------------------------------------------------
open import Data.Fin.Base                          using ( Fin )
open import Data.Fin.Patterns                      using ( 0F ; 1F ; 2F )
open import Data.Product                           using ( Σ-syntax ; _×_ ; _,_ ; proj₁ ; proj₂ )
open import Function                               using ( Func ; id )
open import Level                                  using ( Level ; _⊔_ ; suc )
open import Relation.Binary                        using ( Setoid )
open import Relation.Binary.PropositionalEquality  using ( _≡_ ; refl ; cong ; cong₂ ; setoid )

import Relation.Binary.Reasoning.Setoid as SetoidReasoning

open Func renaming ( to to _⟨$⟩_ ; cong to ≈cong )

-- Imports from the Agda Universal Algebra Library -----------------------------------------------
open import Classical.Operations              using  ( pair ; Curry₂ ; Curry₁ ; Curry₀ )
open import Classical.Signatures.Monoid       using  ( Sig-Monoid ; Op-Monoid )
                                              renaming ( ∙-Op to ∙-Opᵐᵒ ; ε-Op to ε-Opᵐᵒ )
open import Classical.Signatures.Group        using  ( Sig-Group ; Op-Group ; ∙-Op
                                                     ; ε-Op ; ⁻¹-Op ; ar-Group)
open import Classical.Structures.Interpret    using  ( interp-cong )
open import Setoid.Algebras.Reduct            using  ( reductBy )
open import Classical.Structures.Monoid       using  ( Monoid ; _⊨ᵐᵒ_ )
open import Classical.Theories.Group          using  ( Eq-Group ; Th-Group
                                                     ; assoc ; idˡ ; idʳ ; invˡ ; invʳ )
open import Classical.Theories.Monoid         using  ( Th-Monoid )
                                              renaming  ( assoc to assocᵐ
                                                        ; idˡ to idˡᵐ ; idʳ to idʳᵐ )
open import Overture.Operations               using  ( Op )
open import Overture.Terms                    using  ( Term ; ℊ ; node )
open import Overture.Signatures               using  ( ArityOf ; OperationSymbolsOf )
open import Setoid.Algebras.Basic             using  ( Algebra ; _^_ ; 𝔻[_] ; 𝕌[_] ; mkAlgebra )
open import Setoid.Terms                      using  ( module Environment )

open import Setoid.Varieties.EquationalLogic  using  ( _⊧_≈_ )

private variable α ρ : Level

The local satisfaction predicate¶

infix 4 _⊨ᵍᵖ_
_⊨ᵍᵖ_ :  (𝑨 : Algebra {𝑆 = Sig-Group} α ρ)
        (ℰ : Eq-Group → Term (Fin 3) × Term (Fin 3)) → Type (α ⊔ ρ)
𝑨 ⊨ᵍᵖ ℰ = ∀ i → 𝑨 ⊧ proj₁ (ℰ i) ≈ proj₂ (ℰ i)

The type of groups¶

Groupα ρ pairs an algebra over Sig-Group with a proof of Th-Group. Its own signature since the identity is a nullary operation and the inverse is a unary one, and neither can be added to a weaker signature by equations alone. The five equations of Th-Group are associativity, the two unit laws and the two inverse laws.

Group : (α ρ : Level) → Type (suc α ⊔ suc ρ)
Group α ρ = Σ[ 𝑨 ∈ Algebra α ρ ] 𝑨 ⊨ᵍᵖ Th-Group

The reduct to monoids¶

The container morphism Sig-Monoid ⟹ Sig-Group sends the monoid's ∙-Opᵐᵒ and ε-Opᵐᵒ to the group's ∙-Op and ε-Op; the position maps are the identity. group→monoidAlg is the induced reduct of the underlying algebra.

mo-incl : Op-Monoid → Op-Group
mo-incl ∙-Opᵐᵒ = ∙-Op
mo-incl ε-Opᵐᵒ = ε-Op

mo-κ : (o : OperationSymbolsOf Sig-Monoid)
  → ArityOf Sig-Group (mo-incl o) → ArityOf Sig-Monoid o
mo-κ ∙-Opᵐᵒ = id
mo-κ ε-Opᵐᵒ = id

group→monoidAlg : Group α ρ → Algebra {𝑆 = Sig-Monoid} α ρ
group→monoidAlg 𝑮 = reductBy mo-incl mo-κ (𝑮 .proj₁)

Curried associativity, standalone¶

gp-assoc proves x ∙ y ∙ z ≈ x ∙ (y ∙ z) for the group's own ∙, a verbatim port of Monoid-Op.mn-assoc to Sig-Group. It is standalone, above the forgetful projection, so both Group-Op.assoc-law and group→monoid consume one proof.

module _ ((𝑮 , equations) : Group α ρ) where
  open Setoid 𝔻[ 𝑮 ] using (_≈_) renaming (sym to ≈sym ; refl to ≈refl)
  open Environment 𝑮 using ( ⟦_⟧ )
  open SetoidReasoning 𝔻[ 𝑮 ]

  private
    infixl 7 _∙_
    _∙_ : 𝕌[ 𝑮 ] → 𝕌[ 𝑮 ] → 𝕌[ 𝑮 ]
    _∙_ = Curry₂ (∙-Op ^ 𝑮)

    interp-node∙ : (s t : Term (Fin 3)) (η : Fin 3 → 𝕌[ 𝑮 ])
      → ⟦ node ∙-Op (pair s t) ⟧ ⟨$⟩ η ≈ ⟦ s ⟧ ⟨$⟩ η ∙ ⟦ t ⟧ ⟨$⟩ η
    interp-node∙ s t η = interp-cong 𝑮 ∙-Op λ { 0F → ≈refl ; 1F → ≈refl }

  gp-assoc : ∀ x y z → x ∙ y ∙ z ≈ x ∙ (y ∙ z)
  gp-assoc x y z = begin
    x ∙ y ∙ z                ≈˘⟨ interp-cong 𝑮 ∙-Op γ ⟩
    ⟦ node ∙-Op lhs ⟧ ⟨$⟩ η  ≈⟨ equations assoc η ⟩
    ⟦ node ∙-Op rhs ⟧ ⟨$⟩ η  ≈⟨ interp-cong 𝑮 ∙-Op γ' ⟩
    x ∙ (y ∙ z)              ∎
    where
    g0 g1 g2 : Term (Fin 3)
    g0 = ℊ 0F; g1 = ℊ 1F; g2 = ℊ 2F

    η : Fin 3 → 𝕌[ 𝑮 ]
    η = λ { 0F → x ; 1F → y ; 2F → z }

    lhs rhs : Fin 2 → Term (Fin 3)
    lhs = pair (node ∙-Op (pair g0 g1)) g2
    rhs = pair g0 (node ∙-Op (pair g1 g2))

    γ : ∀ i → ⟦ lhs i ⟧ ⟨$⟩ η ≈ pair (x ∙ y) z i
    γ = λ { 0F → interp-node∙ g0 g1 η; 1F → ≈refl }

    γ' : ∀ i → ⟦ rhs i ⟧ ⟨$⟩ η ≈ pair x (y ∙ z) i
    γ' = λ { 0F → ≈refl ; 1F → interp-node∙ g1 g2 η }

The `Group-Op` module¶

Group-Op𝑮 is the named-accessor module for a fixed group, opened at a use site so that the laws read in ordinary notation. It rebuilds the interface from Sig-Group directly rather than inheriting it, because the forgetful to monoids is a reduct along a signature morphism and so carries nothing down.

The three operations come first, curried out of their interpretations: _∙_, ε and _⁻¹. equations is the satisfaction witness projected out of the Σ. Then come the two congruences, ∙-cong and ⁻¹-cong, and the three containment lemmas interp-node-∙, interp-node-ε and interp-node-⁻¹, one per operation symbol, each crossing the gap between a law stated about interpreted terms and the same law in curried form.

The five laws follow: assoc-law, idˡ-law, idʳ-law, invˡ-law and invʳ-law. Each is its equations step wrapped in the containment lemmas for the symbols it mentions, so the inverse laws are the longest of the five: they mention all three operations.

module Group-Op {α ρ : Level} ((𝑮 , equations) : Group α ρ) where
  open Setoid 𝔻[ 𝑮 ] using (_≈_) renaming (trans to ≈trans; sym to ≈sym; refl to ≈refl)
  open SetoidReasoning 𝔻[ 𝑮 ]
  open Environment 𝑮 using ( ⟦_⟧ )

  infixl 7 _∙_
  _∙_ : 𝕌[ 𝑮 ] → 𝕌[ 𝑮 ] → 𝕌[ 𝑮 ]
  _∙_ = Curry₂ (∙-Op ^ 𝑮)

  ε : 𝕌[ 𝑮 ]
  ε = Curry₀ (ε-Op ^ 𝑮)

  infix 8 _⁻¹
  _⁻¹ : 𝕌[ 𝑮 ] → 𝕌[ 𝑮 ]
  _⁻¹ = Curry₁ (⁻¹-Op ^ 𝑮)

  ∙-cong : ∀ {x y u v} → x ≈ y → u ≈ v → x ∙ u ≈ y ∙ v
  ∙-cong x≈y u≈v = interp-cong 𝑮 ∙-Op λ { 0F → x≈y ; 1F → u≈v }

  ⁻¹-cong : ∀ {x y} → x ≈ y → x ⁻¹ ≈ y ⁻¹
  ⁻¹-cong x≈y = interp-cong 𝑮 ⁻¹-Op λ { 0F → x≈y }

  interp-node-∙ : (s t : Term (Fin 3)) {η : Fin 3 → 𝕌[ 𝑮 ]}
    → ⟦ node ∙-Op (pair s t) ⟧ ⟨$⟩ η ≈ ⟦ s ⟧ ⟨$⟩ η ∙ ⟦ t ⟧ ⟨$⟩ η
  interp-node-∙ s t = interp-cong 𝑮 ∙-Op λ { 0F → ≈refl ; 1F → ≈refl }

  interp-node-ε : {η : Fin 3 → 𝕌[ 𝑮 ]} → ⟦ node ε-Op (λ ()) ⟧ ⟨$⟩ η ≈ ε
  interp-node-ε = interp-cong 𝑮 ε-Op (λ ())

  interp-node-⁻¹ : (s : Term (Fin 3)) {η : Fin 3 → 𝕌[ 𝑮 ]}
    → ⟦ node ⁻¹-Op (λ _ → s) ⟧ ⟨$⟩ η ≈ ⟦ s ⟧ ⟨$⟩ η ⁻¹
  interp-node-⁻¹ s = interp-cong 𝑮 ⁻¹-Op λ { 0F → ≈refl }

  assoc-law : ∀ x y z → x ∙ y ∙ z ≈ x ∙ (y ∙ z)
  assoc-law = gp-assoc (𝑮 , equations)

  idˡ-law : ∀ x → ε ∙ x ≈ x
  idˡ-law x = begin
    ε ∙ x                                             ≈˘⟨ ∙-cong interp-node-ε ≈refl ⟩
    ⟦ node ε-Op (λ ()) ⟧ ⟨$⟩ η ∙ ⟦ g0 ⟧ ⟨$⟩ η         ≈˘⟨ interp-node-∙ (node ε-Op (λ ())) g0 ⟩
    ⟦ node ∙-Op (pair (node ε-Op (λ ())) g0) ⟧ ⟨$⟩ η  ≈⟨ equations idˡ η ⟩
    x                                                 ∎
    where
    η : Fin 3 → 𝕌[ 𝑮 ]
    η = λ _ → x

    g0 : Term (Fin 3)
    g0 = ℊ {X = Fin 3} 0F

  idʳ-law : ∀ x → x ∙ ε ≈ x
  idʳ-law x = begin
    x ∙ ε                                             ≈˘⟨ ∙-cong ≈refl interp-node-ε ⟩
    ⟦ g0 ⟧ ⟨$⟩ η ∙ ⟦ node ε-Op (λ ()) ⟧ ⟨$⟩ η         ≈˘⟨ interp-node-∙ g0 (node ε-Op (λ ())) ⟩
    ⟦ node ∙-Op (pair g0 (node ε-Op (λ ()))) ⟧ ⟨$⟩ η  ≈⟨ equations idʳ η ⟩
    x                                                 ∎
    where
    η : Fin 3 → 𝕌[ 𝑮 ]
    η = λ _ → x

    g0 : Term (Fin 3)
    g0 = ℊ {X = Fin 3} 0F

  invˡ-law : ∀ x → x ⁻¹ ∙ x ≈ ε
  invˡ-law x = begin
    x ⁻¹ ∙ x                                       ≈˘⟨ ∙-cong (interp-node-⁻¹ g0 {η}) ≈refl ⟩
    ⟦ node ⁻¹-Op τ ⟧ ⟨$⟩ η ∙ ⟦ g0 ⟧ ⟨$⟩ η          ≈˘⟨ interp-node-∙ (node ⁻¹-Op τ) g0 ⟩
    ⟦ node ∙-Op (pair (node ⁻¹-Op τ) g0) ⟧ ⟨$⟩ η   ≈⟨ equations invˡ η ⟩
    ⟦ node ε-Op (λ ()) ⟧ ⟨$⟩ η                     ≈⟨ interp-node-ε ⟩
    ε              ∎
    where
    η : Fin 3 → 𝕌[ 𝑮 ]
    η = λ _ → x

    τ : (_ : ar-Group ⁻¹-Op) → Term (Fin 3)
    τ = λ _ → ℊ 0F

    g0 : Term (Fin 3)
    g0 = ℊ {X = Fin 3} 0F

  invʳ-law : ∀ x → x ∙ x ⁻¹ ≈ ε
  invʳ-law x = ≈trans  (∙-cong ≈refl (≈sym (interp-node-⁻¹ (ℊ 0F) {λ _ → x})))
                       (≈trans  (≈sym (interp-node-∙ (ℊ 0F) (node ⁻¹-Op (λ _ → ℊ 0F)) {λ _ → x}))
                                (≈trans (equations invʳ (λ _ → x)) (interp-node-ε {λ _ → x})))

The forgetful projection to monoids¶

group→monoid takes a group to the monoid on its (∙, ε)-reduct: the underlying algebra is group→monoidAlg, and the Th-Monoid satisfaction proof pivots through Group-Op's assoc-law, idˡ-law, idʳ-law by the curried-law-pivot pattern of monoid→semigroup, the two identity laws additionally bridging the nullary ε-Op node on the reduct.

group→monoid : Group α ρ → Monoid α ρ
group→monoid 𝒢@(𝑮 , _) = 𝑹 , thm
  where
  𝑹 : Algebra {𝑆 = Sig-Monoid} _ _
  𝑹 = group→monoidAlg 𝒢
  open Setoid 𝔻[ 𝑮 ] using (_≈_) renaming (refl to ≈refl)
  open Environment 𝑹 using ( ⟦_⟧ )    -- Sig-Monoid environment on 𝑹
  open SetoidReasoning 𝔻[ 𝑮 ]
  open Group-Op 𝒢 using ( _∙_ ; ε ; ∙-cong ; assoc-law ; idˡ-law ; idʳ-law )

  -- 𝑹's binary node-bridge, over Sig-Monoid, landing in the group's curried ∙
  interp-node-∙ᴿ : (s t : Term (Fin 3)) (η : Fin 3 → 𝕌[ 𝑮 ])
    → ⟦ node ∙-Opᵐᵒ (pair s t) ⟧ ⟨$⟩ η ≈ ⟦ s ⟧ ⟨$⟩ η ∙ ⟦ t ⟧ ⟨$⟩ η
  interp-node-∙ᴿ s t η = interp-cong 𝑹 ∙-Opᵐᵒ λ { 0F → ≈refl ; 1F → ≈refl }

  -- 𝑹's nullary node-bridge, landing in the group's curried ε
  interp-node-εᴿ : (η : Fin 3 → 𝕌[ 𝑮 ]) → ⟦ node ε-Opᵐᵒ (λ ()) ⟧ ⟨$⟩ η ≈ ε
  interp-node-εᴿ η = interp-cong 𝑹 ε-Opᵐᵒ λ ()

  thm : 𝑹 ⊨ᵐᵒ Th-Monoid
  thm assocᵐ η = begin
    ⟦ Th-Monoid assocᵐ .proj₁ ⟧ ⟨$⟩ η  ≈⟨ interp-node-∙ᴿ xy (ℊ 2F) η ⟩
    ⟦ xy ⟧ ⟨$⟩ η ∙ z                   ≈⟨ ∙-cong (interp-node-∙ᴿ (ℊ 0F) (ℊ 1F) η) ≈refl ⟩
    x ∙ y ∙ z                          ≈⟨ assoc-law x y z ⟩
    x ∙ (y ∙ z)                        ≈˘⟨ ∙-cong ≈refl (interp-node-∙ᴿ (ℊ 1F) (ℊ 2F) η) ⟩
    x ∙ ⟦ yz ⟧ ⟨$⟩ η                   ≈˘⟨ interp-node-∙ᴿ (ℊ 0F) yz η ⟩
    ⟦ Th-Monoid assocᵐ .proj₂ ⟧ ⟨$⟩ η  ∎
    where
    x y z : 𝕌[ 𝑮 ]
    x = η 0F ; y = η 1F ; z = η 2F
    xy yz : Term (Fin 3)
    xy = node ∙-Opᵐᵒ (pair (ℊ 0F) (ℊ 1F))
    yz = node ∙-Opᵐᵒ (pair (ℊ 1F) (ℊ 2F))

  thm idˡᵐ η = begin
    ⟦ Th-Monoid idˡᵐ .proj₁ ⟧ ⟨$⟩ η   ≈⟨ interp-node-∙ᴿ (node ε-Opᵐᵒ λ ()) (ℊ 0F) η ⟩
    ⟦ node ε-Opᵐᵒ (λ ()) ⟧ ⟨$⟩ η ∙ _  ≈⟨ ∙-cong (interp-node-εᴿ η) ≈refl ⟩
    ε ∙ _                             ≈⟨ idˡ-law _ ⟩
    _                                 ∎

  thm idʳᵐ η = begin
    ⟦ Th-Monoid idʳᵐ .proj₁ ⟧ ⟨$⟩ η   ≈⟨ interp-node-∙ᴿ (ℊ 0F) (node ε-Opᵐᵒ λ ()) η ⟩
    _ ∙ ⟦ node ε-Opᵐᵒ (λ ()) ⟧ ⟨$⟩ η  ≈⟨ ∙-cong ≈refl (interp-node-εᴿ η) ⟩
    _ ∙ ε                             ≈⟨ idʳ-law _ ⟩
    _                                 ∎

Group builders¶

opsToBareGroup builds a raw Sig-Group-algebra from a carrier, a binary operation, an identity element, and an inverse, over the propositional-equality setoid setoid A — the empty-theory edge case of the opsTo<family> pattern, now with one clause per Sig-Group symbol.

open Algebra

opsToBareGroup : {A : Type α}
  (_·_ : A → A → A) (e : A) (i : A → A) → Algebra {𝑆 = Sig-Group} α α
opsToBareGroup _·_ e i .Domain = setoid _
opsToBareGroup _·_ e i .Interp ⟨$⟩ (∙-Op , args) = args 0F · args 1F
opsToBareGroup _·_ e i .Interp ⟨$⟩ (ε-Op , _) = e
opsToBareGroup _·_ e i .Interp ⟨$⟩ (⁻¹-Op , args) = i (args 0F)
opsToBareGroup _·_ e i .Interp .≈cong {∙-Op , _} {.∙-Op  , _} (refl , u≈v) = cong₂ _·_ (u≈v 0F) (u≈v 1F)
opsToBareGroup _·_ e i .Interp .≈cong {ε-Op , _} {.ε-Op  , _} (refl , _) = refl
opsToBareGroup _·_ e i .Interp .≈cong {⁻¹-Op , _} {.⁻¹-Op , _} (refl , u≈v) = cong i (u≈v 0F)

eqsToGroup builds a Group from the raw algebra plus the five equation proofs.

eqsToGroup : {A : Type α} (_·_ : A → A → A) (e : A) (i : A → A)
  → (·-assoc : ∀ a b c → (a · b) · c ≡ a · (b · c))
  → (·-idˡ : ∀ a → e · a ≡ a) (·-idʳ : ∀ a → a · e ≡ a)
  → (·-invˡ : ∀ a → (i a) · a ≡ e) (·-invʳ : ∀ a → a · (i a) ≡ e)
  → Group α α
eqsToGroup _·_ e i ·-assoc ·-idˡ ·-idʳ ·-invˡ ·-invʳ = opsToBareGroup _·_ e i , proof
  where
  proof : opsToBareGroup _·_ e i ⊨ᵍᵖ Th-Group
  proof assoc ρ = ·-assoc (ρ 0F) (ρ 1F) (ρ 2F)
  proof idˡ   ρ = ·-idˡ   (ρ 0F)
  proof idʳ   ρ = ·-idʳ   (ρ 0F)
  proof invˡ  ρ = ·-invˡ  (ρ 0F)
  proof invʳ  ρ = ·-invʳ  (ρ 0F)

Setoid-level group builders¶

eqsToGroup covers carriers with propositional equality.

Group constructions in which the carrier is a bona fide setoid (e.g., the wreath product of Classical.Structures.Group.Wreath, whose equality is pointwise-and-pairwise) need a more general form, just as the lattice constructions need setoidEqsToLattice of Classical.Structures.Lattice.Basic.

To address this need, setoidOpsToBareGroup assembles the Sig-Group algebra from a carrier setoid, the three operations, and their congruence proofs (which the propositional case got for free from cong₂).

setoidEqsToGroup adds the five group equations, now stated over the setoid equality ≈.

The interpretation clauses apply the argument tuple (a 0F · a 1F rather than routing through pair), so each equation of Th-Group evaluates definitionally to its curried form and the satisfaction proof consumes the curried hypotheses directly; this is the same reduction discipline as in eqsToGroup above.

module _ (𝐷 : Setoid α ρ) where
  open Setoid 𝐷 using ( _≈_ ) renaming ( Carrier to D ; refl to ≈refl )

  setoidOpsToBareGroup : (_·_ : D → D → D) (e : D) (i : D → D)
    → (∀ {x y u v} → x ≈ y → u ≈ v → x · u ≈ y · v)
    → (∀ {x y} → x ≈ y → i x ≈ i y)
    → Algebra {𝑆 = Sig-Group} α ρ
  setoidOpsToBareGroup _·_ e i ·-cong i-cong = mkAlgebra 𝐷 interp interp-congruence
    where
    interp : (o : OperationSymbolsOf Sig-Group) → Op (ArityOf Sig-Group o) D
    interp ∙-Op   a = a 0F · a 1F
    interp ε-Op   a = e
    interp ⁻¹-Op  a = i (a 0F)

    interp-congruence : ∀ o {u v : ArityOf Sig-Group o → D}
      → (∀ j → u j ≈ v j) → interp o u ≈ interp o v
    interp-congruence ∙-Op   eq = ·-cong (eq 0F) (eq 1F)
    interp-congruence ε-Op   eq = ≈refl
    interp-congruence ⁻¹-Op  eq = i-cong (eq 0F)

  setoidEqsToGroup : (_·_ : D → D → D) (e : D) (i : D → D)
    → (·-cong     : ∀ {x y u v} → x ≈ y → u ≈ v → x · u ≈ y · v)
    → (i-cong     : ∀ {x y} → x ≈ y → i x ≈ i y)
    → (·-assoc-≈  : ∀ a b c → (a · b) · c ≈ a · (b · c))
    → (·-idˡ-≈    : ∀ a → e · a ≈ a)
    → (·-idʳ-≈    : ∀ a → a · e ≈ a)
    → (·-invˡ-≈   : ∀ a → i a · a ≈ e)
    → (·-invʳ-≈   : ∀ a → a · i a ≈ e)
    → Group α ρ
  setoidEqsToGroup _·_ e i ·-cong i-cong ·-assoc-≈ ·-idˡ-≈ ·-idʳ-≈ ·-invˡ-≈ ·-invʳ-≈ =
    setoidOpsToBareGroup _·_ e i ·-cong i-cong , proof
    where
    proof : setoidOpsToBareGroup _·_ e i ·-cong i-cong ⊨ᵍᵖ Th-Group
    proof assoc η = ·-assoc-≈  (η 0F) (η 1F) (η 2F)
    proof idˡ   η = ·-idˡ-≈    (η 0F)
    proof idʳ   η = ·-idʳ-≈    (η 0F)
    proof invˡ  η = ·-invˡ-≈   (η 0F)
    proof invʳ  η = ·-invʳ-≈   (η 0F)