Skip to content

Overture.Signatures.Morphisms

Signature morphisms and the category of signatures

This is the Overture.Signatures.Morphisms module of the Agda Universal Algebra Library.

A signature morphism 𝑆₁ β†’ 𝑆₂ is the Abbott–Altenkirch–Ghani1 container morphism, specialized to the container Signature = (OperationSymbolsOf β–· ArityOf). It is a pair (ΞΉ , ΞΊ): a map ΞΉ sending each operation symbol of 𝑆₁ to one of 𝑆₂ (covariant on symbols), together with a family ΞΊ sending the arity of ΞΉ o back to the arity of o (contravariant on positions). These are exactly the two arguments that reduct consumes today; this module packages them as a first-class record and assembles signatures and their morphisms into a category.

Morphism equality here is propositional (_≑_), not a hom-setoid. Because ΞΉ and ΞΊ are plain functions, the identity morphism is id on both components and composition is ordinary function composition, so the three category laws hold definitionally and are proved by refl: function Ξ· reduces f ∘ id, id ∘ f, and (f ∘ g) ∘ h to f, f, and f ∘ (g ∘ h), and record Ξ· lifts those field equalities to the morphism record. The Fin n Ξ·-gap that forces pointwise reasoning at the stdlib bundle bridges (ADR-002 Β§6) does not arise here, because the laws compose abstract position maps rather than normalizing Fin-pattern lambdas. See ADR-006 for the decision and its rationale.

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

module Overture.Signatures.Morphisms where

-- Imports from Agda and the Agda Standard Library ----------------------------
open import Agda.Primitive                         using () renaming ( Set to Type )
open import Function                               using ( id ; _∘_ )
open import Level                                  using ( _βŠ”_ )
open import Relation.Binary.PropositionalEquality  using ( _≑_ ; refl )

-- Imports from the Agda Universal Algebra Library ----------------------------
-- π“ž / π“₯ are the canonical operation-symbol / arity level variables (ADR-005);
-- imported here, never re-declared.
open import Overture.Signatures
  using ( π“ž ; π“₯ ; Signature ; OperationSymbolsOf ; ArityOf )

private variable
  𝑆 𝑆₁ 𝑆₂ 𝑆₃ 𝑆₄ : Signature π“ž π“₯

Signature morphisms

A SigMorphism 𝑆₁ 𝑆₂ is a container morphism between the signatures-as-containers: the operation-symbol map ΞΉ runs forwards, while for each symbol o the position map ΞΊ o runs backwards, from the arity of ΞΉ o in 𝑆₂ to the arity of o in 𝑆₁. The two signatures are fixed at a common pair of levels (π“ž , π“₯).

record SigMorphism (𝑆₁ 𝑆₂ : Signature π“ž π“₯) : Type (π“ž βŠ” π“₯) where
  constructor mkSigMorphism
  field
    -- covariant on symbols
    ΞΉ : OperationSymbolsOf 𝑆₁ β†’ OperationSymbolsOf 𝑆₂

    -- contravariant on positions
    ΞΊ : (o : OperationSymbolsOf 𝑆₁) β†’ ArityOf 𝑆₂ (ΞΉ o) β†’ ArityOf 𝑆₁ o

open SigMorphism public

Identity and composition

The identity morphism is the identity on symbols and, for each symbol, the identity on positions. Composition runs ΞΉ forwards (covariantly) and ΞΊ backwards (contravariantly): to reindex a position of the composite at o, first pull it back through ψ at ΞΉ Ο† o, then through Ο† at o.

id-morphism : SigMorphism 𝑆 𝑆
id-morphism = record { ΞΉ = id ; ΞΊ = Ξ» _ β†’ id }

infixr 9 _βˆ˜β‚›_

_βˆ˜β‚›_ : SigMorphism 𝑆₂ 𝑆₃ β†’ SigMorphism 𝑆₁ 𝑆₂ β†’ SigMorphism 𝑆₁ 𝑆₃
ψ βˆ˜β‚› Ο† = record { ΞΉ = ΞΉ ψ ∘ ΞΉ Ο† ; ΞΊ = Ξ» o β†’ ΞΊ Ο† o ∘ ΞΊ ψ (ΞΉ Ο† o) }

The category laws

The left and right identity laws and associativity each hold by refl: the relevant function compositions reduce away by Ξ·, and record Ξ· lifts the componentwise equalities to the morphism record. No hom-setoid and no funext are needed.2

βˆ˜β‚›-identityΛ‘ : (Ο† : SigMorphism 𝑆₁ 𝑆₂) β†’ id-morphism βˆ˜β‚› Ο† ≑ Ο†
βˆ˜β‚›-identityΛ‘ _ = refl

βˆ˜β‚›-identityΚ³ : (Ο† : SigMorphism 𝑆₁ 𝑆₂) β†’ Ο† βˆ˜β‚› id-morphism ≑ Ο†
βˆ˜β‚›-identityΚ³ _ = refl

βˆ˜β‚›-assoc : (Ο‡ : SigMorphism 𝑆₃ 𝑆₄) (ψ : SigMorphism 𝑆₂ 𝑆₃) (Ο† : SigMorphism 𝑆₁ 𝑆₂)
  β†’ (Ο‡ βˆ˜β‚› ψ) βˆ˜β‚› Ο† ≑ Ο‡ βˆ˜β‚› (ψ βˆ˜β‚› Ο†)
βˆ˜β‚›-assoc _ _ _ = refl

These four pieces β€” SigMorphism, id-morphism, _βˆ˜β‚›_, and the three laws β€” are exactly the data of a category Sig π“ž π“₯ whose objects are signatures at levels (π“ž , π“₯), and whose realization is self-contained (no agda-categories dependency for now; see ADR-006). Bundling them into a reusable Category record β€” shared with the category of algebras β€” is postponed for follow-up work.

  1. M. Abbott, T. Altenkirch, N. Ghani, Containers: constructing strictly positive types, Theoret. Comput. Sci. 342 (2005) 3–27. ↩

  2. This is the result that ADR-006 records. ↩