Anna Williams, 13 November 2025

The Category of Magmas

\begin{code}

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

open import Categories.Wild
open import Categories.Pre 
open import Categories.Univalent
open import Categories.Notation.Wild renaming (⌜_⌝ to ⌜_⌝')
open import MLTT.Spartan
open import UF.Base
open import UF.Equiv hiding (_≅_) renaming (inverse to e-inverse)
open import UF.FunExt
open import UF.Sets
open import UF.Sets-Properties
open import UF.SIP-Examples
open import UF.Subsingletons
open import UF.Subsingletons-FunExt
open import UF.Subsingletons-Properties
open import UF.Univalence

module Categories.Examples.Magma where

\end{code}

We start by defining the Wild Category of Magmas, using the definition
of Magma from the SIP example for Magma.

\begin{code}

module _ {𝓤 : Universe} (fe : Fun-Ext) where
 open magma renaming (_≅_ to _M≅_)

 MagmaWildCategory : WildCategory (𝓤 ⁺) 𝓤
 MagmaWildCategory = wildcategory Magma
                                  magma-hom
                                  (λ {a} → magma-id {a})
                                  (λ {a} {b} {c} → magma-comp {a} {b} {c})
                                  (λ {a} {b} → left-id-neutral {a} {b})
                                  (λ {a} {b} → right-id-neutral {a} {b})
                                  λ {a} {b} {c} {d}
                                    → magma-assoc {a} {b} {c} {d}
  where
   magma-hom : (a b : Magma) → 𝓤 ̇
   magma-hom (X , _·_ , _)
             (Y , _*_ , _)
    = Σ f ꞉ (X → Y) , ((x y : X) → f (x · y) ＝ f x * f y)

   magma-id : {a : Magma} → magma-hom a a
   magma-id = id , λ x y → refl

   magma-comp : {a b c : Magma}
              → magma-hom b c
              → magma-hom a b
              → magma-hom a c
   magma-comp {X , _·_ , _}
              {Y , _*_ , _}
              {Z , _∙_ , _}
              (f , fp)
              (g , gp) = f ∘ g , ∘-preserves-property
    where
     ∘-preserves-property : (x y : X) → (f ∘ g) (x · y) ＝ (f ∘ g) x ∙ (f ∘ g) y
     ∘-preserves-property x y = (f ∘ g) (x · y)       ＝⟨ ap f (gp x y) ⟩
                                f (g x * g y)         ＝⟨ fp (g x) (g y) ⟩
                                (f ∘ g) x ∙ (f ∘ g) y ∎

   left-id-neutral : {a b : Magma}
                     (f : magma-hom a b)
                   → magma-comp {a} {b} {b} (magma-id {b}) f ＝ f
   left-id-neutral {_} {_ , _ , sB} (f , pf)
    = to-Σ-＝ (refl , dfunext fe (λ x → dfunext fe (λ y → sB _ _)))

   right-id-neutral : {a b : Magma}
                      (f : magma-hom a b)
                    → magma-comp {a} {a} {b} f (magma-id {a}) ＝ f
   right-id-neutral {_} {_ , _ , sB} (f , pf)
    = to-Σ-＝ (refl , dfunext fe (λ x → dfunext fe (λ y → sB _ _)))

   magma-assoc : {a b c d : Magma}
                 (f : magma-hom a b)
                 (g : magma-hom b c)
                 (h : magma-hom c d)
               → magma-comp {a} {c} {d} h (magma-comp {a} {b} {c} g f)
               ＝ magma-comp {a} {b} {d} (magma-comp {b} {c} {d} h g) f
   magma-assoc {_} {_} {_} {_ , _ , sD} (f , pf) (g , pg) (h , ph)
    = to-Σ-＝ (refl , dfunext fe (λ x → dfunext fe (λ y → sD _ _)))

 open WildCategoryNotation MagmaWildCategory

\end{code}

We now show that this is a precategory

\begin{code}

 MagmaPrecategory : Precategory (𝓤 ⁺) 𝓤
 MagmaPrecategory = MagmaWildCategory , is-pre
  where
   is-pre : is-precategory MagmaWildCategory
   is-pre (_ , _ , sX) (_ , _ , sY)
    = Σ-is-set (Π-is-set fe (λ _ → sY))
       λ f → Π₂-is-set fe
         λ x y → props-are-sets sY

\end{code}

We show that Magmas have univalence, using the SIP example for Magmas. To do
this, we show that the notion of isomorphism for the sip example is equivalent
to that of isomorphism in the magma wild category.

\begin{code}

 sns-equiv-iso : (A B : Magma)
               → (A M≅ B) ≃ (A ≅ B)
 sns-equiv-iso A@(a , _·_ , sA) B@(b , _*_ , sB)
  = qinveq toiso (fromiso , has-section , is-section)
  where
   toiso : A M≅ B → A ≅ B
   toiso (f , e@((g , gp) , (g' , gp')) , fp)
         = (f , λ x y → ap (λ - → - x y) fp)
         , (g , g-is-hom)
         , to-subtype-＝ left-is-prop (e-inverse _ (fe _ _) left-inv)
         , to-subtype-＝ right-is-prop (e-inverse _ (fe _ _) gp)
    where
     g-is-hom : (x y : b) → g (x * y) ＝ (g x · g y)
     g-is-hom x y = g (x * y)             ＝⟨ i ⟩
                    g (f (g x) * y)       ＝⟨ ii ⟩
                    g (f (g x) * f (g y)) ＝⟨ iii ⟩
                    g (f (g x · g y))     ＝⟨ iv ⟩
                    g x · g y             ∎
      where
       i   = ap (λ - → g (- * y)) (gp x)⁻¹
       ii  = ap (λ - → g (f (g x) * -)) (gp y)⁻¹
       iii = ap g ((λ x y → ap (λ - → - x y) fp) (g x) (g y))⁻¹
       iv  = inverses-are-retractions f e (g x · g y)

     left-is-prop = (λ _ → Π₂-is-prop fe (λ _ _ → sA))
     right-is-prop = (λ _ → Π₂-is-prop fe (λ _ _ → sB))
     
     left-inv : (λ x → g (f x)) ∼ (λ x → x)
     left-inv = inverses-are-retractions f e
     
   fromiso : A ≅ B → A M≅ B
   fromiso ((f , fp) , (g , gp) , lg , rg)
    = f
    , f-is-equiv
    , dfunext fe (λ x → dfunext fe (λ y → fp x y))

    where
     f-is-equiv = (g , λ x → ap (λ - → - x) (ap pr₁ rg))
                , (g , λ x → ap (λ - → - x) (ap pr₁ lg))

   is-section : toiso ∘ fromiso ∼ id
   is-section e@((f , fp) , (g , gp) , lg , rg)
    = to-Σ-＝ (to-subtype-＝ (λ _ → Π₂-is-prop fe (λ x y → sB)) refl
    , to-Σ-＝ (at-most-one-inverse {_} {_} {_} {A} {B} {(f , fp)}
                to-from-inv id-inv
    , to-×-＝ (hom-is-set MagmaPrecategory {A} {A} _ _)
              (hom-is-set MagmaPrecategory {B} {B} _ _)))
    where
     isomorphism = ⌜_⌝' {_} {_} {_} {A} {B} ((toiso ∘ fromiso)
                                             ((f , fp) , (g , gp) , lg , rg))
     iso-inverse = inverse {_} {_} {_} {A} {B}

     isomorphism-is-iso : iso-inverse isomorphism
     isomorphism-is-iso
      = underlying-morphism-is-isomorphism {_} {_} {_} {A} {B}
                                           ((toiso ∘ fromiso) e)

     isomorphism-equality : (e : isomorphism ＝ f , fp)
                          → iso-inverse isomorphism
                          → iso-inverse (f , fp)
     isomorphism-equality e first = transport iso-inverse e first

     to-from-inv id-inv : iso-inverse (f , fp)
     to-from-inv = isomorphism-equality
                    (to-subtype-＝ (λ _ → Π₂-is-prop fe (λ x y → sB))
                                   refl)
                    isomorphism-is-iso
     id-inv = ((g , gp) , lg , rg)
   
   has-section : fromiso ∘ toiso ∼ id
   has-section (f , e@((g , gp) , (g' , gp')) , fp)
    = to-Σ-＝ (refl
            , (to-×-＝ is-equiv-f-＝ (Π₂-is-set fe (λ _ _ → sB) _ _)))
    where
     is-equiv-f-＝ = (to-×-＝
                 (to-subtype-＝ (λ p → Π-is-prop fe λ y → sB) refl)
                 (to-subtype-＝ (λ p → Π-is-prop fe λ y → sA) invs-eq))

      where
       invs-eq : g ＝ g'
       invs-eq = dfunext fe λ b → g b            ＝⟨ (gp' (g b))⁻¹ ⟩
                                  (g' ∘ f ∘ g) b ＝⟨ ap g' (gp b) ⟩
                                  g' b           ∎

 characterization-of-magma-＝ : is-univalent 𝓤
                             → (A B : Magma)
                             → (A ＝ B) ≃ (A ≅ B)
 characterization-of-magma-＝ ua A B = ≃-comp
                                       (characterization-of-Magma-＝ ua A B)
                                       (sns-equiv-iso A B)

\end{code}

And finally show that this is a category.

\begin{code}

 MagmaCategory : is-univalent 𝓤 → Category (𝓤 ⁺) 𝓤
 MagmaCategory ua = MagmaPrecategory , is-cat
  where
   pointwise-eq : (A B : Magma)
      → id-to-iso A B
      ∼ ⌜ characterization-of-magma-＝ ua A B ⌝
   pointwise-eq A@(a , _·_ , sA) B@(b , _*_ , sB) refl
    = to-Σ-＝ (refl , underlying-equality)
    where
     inv-eq' = to-subtype-＝ (λ f → Π₂-is-prop fe (λ _ _ → sB)) refl

     left-inv = hom-is-set MagmaPrecategory {A} {A} _ _
     right-inv = hom-is-set MagmaPrecategory {A} {A} _ _
    
     underlying-is-iso = underlying-morphism-is-isomorphism {_} {_} {_} {A} {B}

     underlying-equality : underlying-is-iso ((id-to-iso A B) refl)
                         ＝ underlying-is-iso 
                            (⌜ characterization-of-magma-＝ ua A B ⌝ refl) 
     underlying-equality = to-Σ-＝ (inv-eq' , to-×-＝ left-inv right-inv)

   is-cat : is-category MagmaPrecategory
   is-cat A B = equiv-closed-under-∼
                 ⌜ characterization-of-magma-＝ ua A B ⌝
                 (id-to-iso A B)
                 ⌜ characterization-of-magma-＝ ua A B ⌝-is-equiv
                 (pointwise-eq A B)

\end{code}