Skip to content

Setoid.Categories.Category

A minimal category with a hom-setoid

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

A category is the simplest mathematical setting in which one can speak of objects and of structure-preserving passages between them, without saying what the objects are made of. The data is: a collection of objects; for each pair of objects a collection of morphisms (Hom A B, drawn as arrows A ⟢ B); an identity arrow on every object; and a composition taking g : B ⟢ C and f : A ⟢ B to g ∘ f : A ⟢ C. The laws β€” associativity of composition and the two identity laws β€” are exactly the monoid axioms, generalized to a setting where two arrows compose only when their endpoints match. That is the right level of generality for this library's purposes: the categories we care about have algebras (or signatures, or setoids) as objects and homomorphisms (or signature morphisms, or setoid functions) as arrows, and theorems stated at the category level β€” functoriality, adjointness, monad laws β€” then apply to all of them at once. The reader who wants a single mental picture should hold on to the category of 𝑆-algebras: objects are algebras, arrows are homomorphisms, composition is composition of maps (Alg).

Category o β„“ e is a self-contained, agda-categories-free category record: objects in Type o, hom types in Type β„“, and a per-hom-set equivalence _β‰ˆ_ valued in Type e.

The one departure from the textbook definition deserves emphasis, because it is forced by the constructive setting and recurs throughout the layer. Classically one says two morphisms simply are or are not equal; here every hom-set carries its own equivalence relation _β‰ˆ_, supplied as a field, and all laws are stated against it. Carrying _β‰ˆ_ as a field β€” rather than fixing it to propositional _≑_ β€” is what lets the category of algebras use pointwise homomorphism equality ("the underlying maps agree on every element"), which _≑_ cannot express under --safe without function extensionality. The two instances built so far sit at the two extremes (ADR-006): the category Sig of signatures uses _≑_ and proves its laws by refl (Overture.Signatures.Morphisms), while the category Alg 𝑆 of algebras uses the pointwise hom-setoid _≋_ (Setoid.Categories.Algebra). One record accommodates both precisely because the hom-equality is data.

The record is deliberately minimal β€” exactly the data and laws we need to express reducts as functors, adjunctions, and monads β€” and is pure Type-level category theory (no Setoid import). It lives under Setoid.Categories because its current consumers are setoid-based. The rest of the vocabulary builds on it in order: Functor (translations between categories), NaturalTransformation (comparisons between translations), Adjunction (free ⊣ forgetful pairs), and Monad (formal-expression structure, e.g. terms-with-substitution).

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

module Setoid.Categories.Category where

open import Agda.Primitive  using ( _βŠ”_ ; lsuc ) renaming ( Set to Type )
open import Level           using ( Level )
open import Relation.Binary using ( IsEquivalence )

private variable o β„“ e : Level

record Category (o β„“ e : Level) : Type (lsuc (o βŠ” β„“ βŠ” e)) where
  infixr 9 _∘_
  infix 4 _β‰ˆ_

  field
    Obj  : Type o
    Hom  : Obj β†’ Obj β†’ Type β„“
    _β‰ˆ_  : {A B : Obj} β†’ Hom A B β†’ Hom A B β†’ Type e
    id   : {A : Obj} β†’ Hom A A
    _∘_  : {A B C : Obj} β†’ Hom B C β†’ Hom A B β†’ Hom A C

    β‰ˆ-equiv    :  {A B : Obj} β†’ IsEquivalence (_β‰ˆ_ {A} {B})
    assoc      :  {A B C D : Obj} {f : Hom A B} {g : Hom B C} {h : Hom C D}
                  β†’ (h ∘ g) ∘ f β‰ˆ h ∘ (g ∘ f)
    identityΛ‘  :  {A B : Obj} {f : Hom A B} β†’ id ∘ f β‰ˆ f
    identityΚ³  :  {A B : Obj} {f : Hom A B} β†’ f ∘ id β‰ˆ f
    ∘-resp-β‰ˆ   :  {A B C : Obj} {f g : Hom B C} {h i : Hom A B}
                  β†’ f β‰ˆ g β†’ h β‰ˆ i β†’ f ∘ h β‰ˆ g ∘ i

  -- Reflexivity, symmetry, and transitivity of each hom-set's equivalence,
  -- surfaced for use in functor-law and instance proofs.
  β‰ˆ-refl : {A B : Obj} {f : Hom A B} β†’ f β‰ˆ f
  β‰ˆ-refl = IsEquivalence.refl β‰ˆ-equiv

  β‰ˆ-sym : {A B : Obj} {f g : Hom A B} β†’ f β‰ˆ g β†’ g β‰ˆ f
  β‰ˆ-sym = IsEquivalence.sym β‰ˆ-equiv

  β‰ˆ-trans : {A B : Obj} {f g h : Hom A B} β†’ f β‰ˆ g β†’ g β‰ˆ h β†’ f β‰ˆ h
  β‰ˆ-trans = IsEquivalence.trans β‰ˆ-equiv