Skip to content

Setoid.Algebras.Reduct

Signature reducts along a signature morphism

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

A reduct of an 𝑆₂-algebra 𝑨 along a signature morphism Ο† : 𝑆₁ β†’ 𝑆₂ is the 𝑆₁-algebra with the same carrier whose operations are those of 𝑨 named by Ο†, interpreted exactly as in 𝑨. Reduct is a construction of general universal algebra β€” it acts on algebras over arbitrary signatures along an arbitrary signature morphism β€” so its home is the Setoid/ foundation, relocated here from Classical/ by ADR-006 (M4-16; see the Amendment). Its principal consumers, however, are classical: it is the first non-proj₁ forgetful projection in the structure hierarchy (per ADR-002 v2 Β§5); monoidβ†’semigroup and groupβ†’monoid are reducts (composed with an equation-reindex), whereas semigroupβ†’magma, commutativeMonoidβ†’monoid, and abelianGroupβ†’group are proj₁.

We take the container-morphism form rather than an arity-equation form. A signature inclusion is a SigMorphism (ΞΉ , ΞΊ): ΞΉ maps operation symbols of 𝑆₁ to symbols of 𝑆₂ (covariantly), and ΞΊ maps the arity of ΞΉ o back to the arity of o (contravariantly). This induces the polynomial-functor natural transformation P_{𝑆₁} ⟹ P_{𝑆₂}, and reduct Ο† precomposes the 𝑆₂-structure map with it. Two payoffs over an ArityOf 𝑆₁ o ≑ ArityOf 𝑆₂ (ΞΉ o) formulation: 1. the interpretation is plain function composition args ∘ ΞΊ Ο† o with no subst, keeping proof terms transport-free (and the Cubical port mechanical); 2. for an arity-preserving inclusion ΞΊ Ο† o is id, so the reduct preserves each retained symbol's interpretation definitionally, which is what discharges the downstream theory-reindex obligation cheaply.

The container morphism is packaged as follows: reduct consumes a SigMorphism, with reductBy retaining the two-argument form as a thin wrapper. Packaging makes reduct a (contravariant) functor β€” reduct-id and reduct-∘ below state identity- and composition-preservation, both holding by refl.

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

open import Overture using ( π“ž ; π“₯ ; Signature )

module Setoid.Algebras.Reduct where

-- Imports from Agda and the Agda Standard Library ----------------------------
open import Data.Product                          using ( _,_ )
open import Function                              using ( _∘_ ; _βˆ˜β‚‚_ ; Func )
open import Level                                 using ( Level )
open import Relation.Binary.PropositionalEquality using (_≑_; refl)

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

-- Imports from the Agda Universal Algebra Library ----------------------------
open import Overture.Signatures            using  ( OperationSymbolsOf ; ArityOf )
open import Overture.Signatures.Morphisms  using  ( SigMorphism ; mkSigMorphism
                                                  ; ΞΉ ; ΞΊ ; id-morphism ; _βˆ˜β‚›_ )
open import Setoid.Algebras.Basic          using  ( Algebra ; _^_ ; π•Œ[_] )
private variable
  α ρ : Level
  𝑆 𝑆₁ 𝑆₂ 𝑆₃ : Signature π“ž π“₯

The reduct of an algebra along a signature morphism

reduct Ο† 𝑨 is the 𝑆₁-algebra obtained from the 𝑆₂-algebra 𝑨 by the signature morphism Ο† : SigMorphism 𝑆₁ 𝑆₂. The domain is unchanged; the interpretation of a symbol o of 𝑆₁ is the interpretation of ΞΉ Ο† o in 𝑨, with arguments reindexed through ΞΊ Ο† o. Both signatures are passed implicitly at the use site, recovered from the type of Ο†.

reduct : SigMorphism 𝑆₁ 𝑆₂ β†’ Algebra {𝑆 = 𝑆₂} Ξ± ρ β†’ Algebra {𝑆 = 𝑆₁} Ξ± ρ
reduct Ο† 𝑨 .Algebra.Domain = Algebra.Domain 𝑨
reduct Ο† 𝑨 .Algebra.Interp ⟨$⟩ (o , args) = (ΞΉ Ο† o ^ 𝑨) (args ∘ ΞΊ Ο† o)
reduct Ο† 𝑨 .Algebra.Interp .cong {o , u} {.o , u'} (refl , uβ‰ˆv) =
  cong (Algebra.Interp 𝑨) (refl , Ξ» i β†’ uβ‰ˆv (ΞΊ Ο† o i))

The two-argument form is retained as a thin wrapper, so a call site that already holds ΞΉ and ΞΊ separately need not assemble the record by hand.

reductBy : {𝑆₁ 𝑆₂ : Signature π“ž π“₯}
  (ΞΉ : OperationSymbolsOf 𝑆₁ β†’ OperationSymbolsOf 𝑆₂)
  (ΞΊ : (o : OperationSymbolsOf 𝑆₁) β†’ ArityOf 𝑆₂ (ΞΉ o) β†’ ArityOf 𝑆₁ o)
  β†’ Algebra {𝑆 = 𝑆₂} Ξ± ρ β†’ Algebra {𝑆 = 𝑆₁} Ξ± ρ
reductBy = reduct βˆ˜β‚‚ mkSigMorphism

Functoriality

reduct is functorial in the signature morphism, contravariantly: it preserves the identity and turns a composite into the reversed composite of reducts. Following the strict-first discipline, each law is stated at the level of an operation's interpretation function (o ^ reduct … ≑ o ^ …, with no argument tuple applied) and holds by refl; the conventional args-applied functoriality statement is the corollary directly below each (also refl β€” it is the strict law specialized to an argument tuple). This is the strongest equality --safe affords short of equating the algebras themselves, which would need funext for the Interp.cong field.

reduct-id : {𝑨 : Algebra {𝑆 = 𝑆} Ξ± ρ} {o : OperationSymbolsOf 𝑆}
  β†’ o ^ reduct id-morphism 𝑨 ≑ o ^ 𝑨
reduct-id = refl

reduct-id-ptw : {𝑨 : Algebra {𝑆 = 𝑆} Ξ± ρ} {o : OperationSymbolsOf 𝑆}
  (args : ArityOf 𝑆 o β†’ π•Œ[ 𝑨 ]) β†’ (o ^ reduct id-morphism 𝑨) args ≑ (o ^ 𝑨) args
reduct-id-ptw _ = refl

reduct-∘ : {𝑆₁ 𝑆₂ 𝑆₃ : Signature π“ž π“₯}
  {Ο† : SigMorphism 𝑆₁ 𝑆₂} {ψ : SigMorphism 𝑆₂ 𝑆₃}
  {𝑨 : Algebra {𝑆 = 𝑆₃} Ξ± ρ} {o : OperationSymbolsOf 𝑆₁}
  β†’ o ^ reduct (ψ βˆ˜β‚› Ο†) 𝑨 ≑ o ^ reduct Ο† (reduct ψ 𝑨)
reduct-∘ = refl

reduct-∘-ptw : {𝑆₁ 𝑆₂ 𝑆₃ : Signature π“ž π“₯}
  {Ο† : SigMorphism 𝑆₁ 𝑆₂} {ψ : SigMorphism 𝑆₂ 𝑆₃}
  {𝑨 : Algebra {𝑆 = 𝑆₃} Ξ± ρ} {o : OperationSymbolsOf 𝑆₁}
  (args : ArityOf 𝑆₁ o β†’ π•Œ[ 𝑨 ])
  β†’ (o ^ reduct (ψ βˆ˜β‚› Ο†) 𝑨) args ≑ (o ^ reduct Ο† (reduct ψ 𝑨)) args
reduct-∘-ptw _ = refl