Setoid.Categories.Reduct

Reduct as a functor on algebras

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

A signature morphism φ : SigMorphism 𝑆₁ 𝑆₂ induces a covariant functor reductF φ : Alg 𝑆₂ ⟶ Alg 𝑆₁ between the algebra categories. On objects it is reductφ; on a homomorphism it keeps the same underlying setoid map and transfers the 𝑆₂-homomorphism condition to 𝑆₁ by the κ-reindex — compatible at the 𝑆₁-symbol o is f's 𝑆₂-compatible at ι φ o, definitionally on the nose, because (o ^ reduct φ 𝑨) = (ι φ o ^ 𝑨) ∘ (_∘ κ φ o).

The functor laws are immediate: F-resp-≈ is the identity (the underlying maps are unchanged, and the hom-equality is pointwise on them), and identity / homomorphism hold by the codomain's refl (the underlying maps of both sides are the same — 𝒾𝒹 and ⊙-hom are the identity map and function composition).

This functor lives in Setoid.Categories, alongside the rest of the category vocabulary; its object map reduct is Setoid.Algebras.Reduct, also a Setoid/ construction. (Both were relocated from Classical/ by ADR-006, M4-16: reduct is universal algebra, not classical, and depends on nothing in Classical/.)

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

module Setoid.Categories.Reduct where

-- Imports from the Agda Standard Library ----------------------------
open import Data.Product                   using ( _,_ ; proj₁ ; proj₂ )
open import Function                       using ( Func ; _∘_ ; id)
open import Level                          using ( Level )
open import Relation.Binary                using ( Setoid )

-- Imports from the Agda Universal Algebra Library ----------------------------
open import Overture                       using ( 𝓞 ; 𝓥 ; Signature )
open import Overture.Signatures.Morphisms  using ( SigMorphism ; ι ; κ )
open import Setoid.Algebras.Basic          using ( 𝔻[_] )
open import Setoid.Algebras.Reduct         using ( reduct )
open import Setoid.Categories.Algebra      using ( Alg)
open import Setoid.Categories.Functor      using ( Functor )
open import Setoid.Homomorphisms.Basic     using ( IsHom ; mkIsHom)

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

private variable
  α ρ : Level

open IsHom

reductF : {𝑆₁ 𝑆₂ : Signature 𝓞 𝓥} (φ : SigMorphism 𝑆₁ 𝑆₂)
  → Functor (Alg {𝑆 = 𝑆₂} α ρ) (Alg {𝑆 = 𝑆₁} α ρ)
reductF φ =
  record
    { F₀            = reduct φ
    ; F₁            = λ f →  proj₁ f
                             , mkIsHom λ{o a} → compatible (proj₂ f) {ι φ o} {a ∘ κ φ o}
    ; F-resp-≈      = id
    ; identity      = λ {𝑨} _ → Setoid.refl 𝔻[ reduct φ 𝑨 ]
    ; homomorphism  = λ {_} {_} {E} _ → Setoid.refl 𝔻[ reduct φ E ]
    }