Magmas, Monoids, Groups

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

module structures where 

open import mltt
open import twocatconstructions
open import sets-logic
open import basichomotopy

open ≡-Reasoning
open ◾-lemmas
open ~-lemmas

We start a module to hold the Magma axioms. Recall that (in ordinary Mathematics) a magma is a set with a binary operation satisfying no conditions.

module Magmas where

  record Magma (ℓ : Level) : Set (lsuc ℓ) where
    constructor magma
    field
      -- Unicode with '\|', not a '|' which causes a syntax error
      ∣_∣ : Set ℓ
      is  : isSet ∣_∣
      _•_ : ∣_∣ → ∣_∣ → ∣_∣
--      m   : ∣_∣ → ∣_∣ → ∣_∣
--    syntax m M x y = x •[ M ] y

  open Magma

The reason for the above ‘syntax’ declaration is that without it, M occurs before the terms x y, which are of type ∣ M ∣. We also open the record (inside the module, though) to avoid prepending with Magma. to qualify the field names.

We define Magma homomorphisms, which are the obvious thing, and we state that the identity function of the underlying type id {A = ∣ X ∣} is a homomorphism. Note the condition that the carrier be a set does not enter into the definition of homomorphism.

  record Magma-Hom {ℓ ℓ' : Level} (X : Magma ℓ) (Y : Magma ℓ') : Set (ℓ ⊔ ℓ') where
    private
      module X = Magma X
      module Y = Magma Y
    field
      f : ∣ X ∣ → ∣ Y ∣
      c : (x y : ∣ X ∣) → f ( x X.• y ) ≡ f x Y.• f y
--      c : (x y : ∣ X ∣) → f ( x •[ X ] y ) ≡ f x  •[ Y ] f y

  id-Magma-Hom : ∀ {ℓ} (X : Magma ℓ) → Magma-Hom X X
  Magma-Hom.f (id-Magma-Hom X) = id {A = ∣ X ∣}
  Magma-Hom.c (id-Magma-Hom X) = λ x y → refl

We define isomorphisms in the obvious way: if φ : X → Y is a magma homomorphism, it is an iso if there is a homomorphims ψ : Y → X such that the two compositions of the underlying set maps are the identity.

  record Magma-Iso {ℓ ℓ' : Level} (X : Magma ℓ) (Y : Magma ℓ') : Set (ℓ ⊔ ℓ') where
    open Magma-Hom
    field
      φ : Magma-Hom X Y
      ψ : Magma-Hom Y X
      ε : (f φ) ∘′ (f ψ) ~ id
      η : (f ψ) ∘′ (f φ) ~ id

Of course, the identity is a magma isomorphism:

  id-Magma-Iso : ∀ {ℓ} (X : Magma ℓ) → Magma-Iso  X X
  Magma-Iso.φ (id-Magma-Iso X) = id-Magma-Hom X
  Magma-Iso.ψ (id-Magma-Iso X) = id-Magma-Hom X
  Magma-Iso.ε (id-Magma-Iso X) = λ x → refl
  Magma-Iso.η (id-Magma-Iso X) = λ x → refl

Identification between magmas (at the same level) give isomorphisms, by path induction and using that the identity is an isomorphism.

  Id-Magma→Magda-Iso : ∀ {ℓ} {X Y : Magma ℓ} → X ≡ Y → Magma-Iso X Y
  Id-Magma→Magda-Iso refl = id-Magma-Iso _

Note that in an isomorphism the underlying function is a weak equivalence. Thus in the presence of univalence the types X ≡ Y and Magma-Iso X Y would be in bijection, but this requires a careful preliminary analysis of the identity type X ≡ Y.

  Magma→Σ : ∀ {ℓ} → Magma ℓ → Σ[ M ∈ Set ℓ ] ((isSet M) × (M → M → M))
  Magma→Σ {ℓ} X = ∣ X ∣ , (is X , _•_ X)

  Σ→Magma : ∀ {ℓ} → Σ[ M ∈ Set ℓ ] ((isSet M) × (M → M → M)) → Magma ℓ
  Σ→Magma {ℓ} (M , is , m) = record { ∣_∣ = M ; is = is ; _•_ = m }

  ≡-η-equality : ∀ {ℓ} (X Y : Magma ℓ) ( p : ∣ X ∣ ≡ ∣ Y ∣ ) → 
                                       ( transport (λ A → isSet A) p (is X)  ≡ is Y ) → 
                                       ( transport (λ A → A → A → A) p (_•_ X) ≡ _•_ Y) → 
                                       X ≡ Y
  ≡-η-equality (magma A₁ is₁ _•_₁) (magma .A₁ is₂ _•_₂) refl γ δ = magma A₁ is₁ _•_₁ ≡⟨ ap (λ v → magma A₁ v _•_₁) γ ⟩
                                                                   magma A₁ is₂ _•_₁ ≡⟨ ap (λ v → magma A₁ is₂ v) δ ⟩
                                                                   magma A₁ is₂ _•_₂ ∎

  magma-transport : ∀ {ℓ} (X : Magma ℓ) (B : Set ℓ) (is : isSet B) (p : ∣ X ∣ ≡ B) → Magma ℓ
  magma-transport X B is p = magma B is (transport (λ Z → Z → Z → Z) p (_•_ X))

top ⇑

Contents