Setoid.Categories.Algebra

The category of 𝑆-algebras

This is the Setoid.Categories.Algebra module of the Agda Universal Algebra Library.

Alg 𝑆 α ρ assembles the 𝑆-algebras at levels (α , ρ) into a Category:

• objects inhabit Algebra α ρ,
• homs are the setoid homomorphisms hom of Setoid.Homomorphisms,
• identity and composition are the 𝒾𝒹 and ⊙-hom of Setoid.Homomorphisms
• the hom-equality _≋_ is defined in this module and is pointwise equality: two homomorphisms are equal when their underlying maps agree on every element, in the codomain's setoid equality.

Pointwise hom-setoid equality is exactly what _≡_ cannot provide under --safe, and is why the Category record carries _≈_ as a field.

The associative and identity laws hold by the codomain's refl (the underlying maps are definitionally equal; ⊙-hom is function composition, 𝒾𝒹 the identity map); ∘-resp-≈ is the one law with content, combining the codomain's trans with a hom's cong.

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

module Setoid.Categories.Algebra where

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

-- Imports from the Agda Standard Library -----------------------------------
open import Data.Product     using ( proj₁ )
open import Function         using ( Func )
open import Level            using ( Level ; _⊔_ ) renaming ( suc to lsuc )
open import Relation.Binary  using ( Setoid ; IsEquivalence )

-- Imports from the Agda Universal Algebra Library ----------------------------
open import Overture                         using ( 𝓞 ; 𝓥 ; Signature ; 𝑆 )
open import Setoid.Algebras.Basic            using ( Algebra ; 𝕌[_] ; 𝔻[_] )
open import Setoid.Homomorphisms.Basic       using ( hom ; 𝒾𝒹 )
open import Setoid.Homomorphisms.Properties  using ( ⊙-hom )
open import Setoid.Categories.Category       using ( Category )

open Func using (cong) renaming ( to to _⟨$⟩_ )

private variable α ρ : Level

Pointwise equality of homomorphisms

_≋_ : {𝑆 : Signature 𝓞 𝓥}{𝑨 𝑩 : Algebra {𝑆 = 𝑆} α ρ} → hom 𝑨 𝑩 → hom 𝑨 𝑩 → Type (α ⊔ ρ)
_≋_ {𝑨 = 𝑨} {𝑩} f g = ∀ (x : 𝕌[ 𝑨 ]) → Setoid._≈_ 𝔻[ 𝑩 ] (proj₁ f ⟨$⟩ x) (proj₁ g ⟨$⟩ x)

≋-equiv : {𝑆 : Signature 𝓞 𝓥}{𝑨 𝑩 : Algebra {𝑆 = 𝑆} α ρ} → IsEquivalence (_≋_ {𝑨 = 𝑨} {𝑩})
≋-equiv {𝑩 = 𝑩} = record
  { refl = λ _ → Setoid.refl 𝔻[ 𝑩 ]
  ; sym = λ f≋g x → Setoid.sym 𝔻[ 𝑩 ] (f≋g x)
  ; trans = λ f≋g g≋h x → Setoid.trans 𝔻[ 𝑩 ] (f≋g x) (g≋h x)
  }

The category

Alg α ρ is the category of 𝑆-algebras at a fixed pair of levels: objects are algebras, morphisms are homomorphisms, and two morphisms are identified when they agree pointwise up to the codomain's equality (_≋_, defined above).

Everything the Category record asks for is already at hand. The identity is 𝒾𝒹 and composition is ⊙-hom with its arguments flipped, since ⊙-hom takes them in diagrammatic order while a category's _∘_ does not. Associativity and both unit laws hold on the nose under _≋_, so each is discharged by reflexivity of the codomain's equality; only ∘-resp-≈ needs an argument, and that argument is congruence of the underlying setoid functions.

Alg : {𝑆 : Signature 𝓞 𝓥}(α ρ : Level) → Category (𝓞 ⊔ 𝓥 ⊔ lsuc (α ⊔ ρ)) (𝓞 ⊔ 𝓥 ⊔ α ⊔ ρ) (α ⊔ ρ)
Alg {𝑆 = 𝑆} α ρ = record
  { Obj       = Algebra {𝑆 = 𝑆} α ρ
  ; Hom       = hom
  ; _≈_       = _≋_
  ; id        = 𝒾𝒹
  ; _∘_       = λ g f → ⊙-hom f g
  ; ≈-equiv   = ≋-equiv
  ; assoc     = λ {_} {_} {_} {𝑫} _ → Setoid.refl 𝔻[ 𝑫 ]
  ; identityˡ = λ {_} {𝑩} _ → Setoid.refl 𝔻[ 𝑩 ]
  ; identityʳ = λ {_} {𝑩} _ → Setoid.refl 𝔻[ 𝑩 ]
  ; ∘-resp-≈  = λ {_} {_} {𝑪} {_} {g} {h} f≋g h≋i x →
                  Setoid.trans 𝔻[ 𝑪 ] (f≋g (proj₁ h ⟨$⟩ x)) (cong (proj₁ g) (h≋i x))
  }