Synthetic category theory

Volume I Β· Experimental web edition

SCT.Calculus.Composition

Other Agda modules in this folder (2)

Complete compiler-highlighted source. Follow a symbol to its declaration.

# Composition and cancellation

We separate composition from its laws. The comparison type retains the
specified witnesses: it is not Agda equality, and no uniqueness of comparison
proofs is assumed. These records are interfaces for calculations, not a new
definition of synthetic category.

```agda
{-# OPTIONS --safe --without-K #-}
module SCT.Calculus.Composition where

open import Agda.Primitive using (Level; lsuc; _βŠ”_)

record Composition (o h p : Level) : Set (lsuc (o βŠ” h βŠ” p)) where
  infixr 30 _∘_
  infix 10 _β‰ˆ_
  field
    Obj : Set o
    Hom : Obj β†’ Obj β†’ Set h
    _β‰ˆ_ : {x y : Obj} β†’ Hom x y β†’ Hom x y β†’ Set p
    id : (x : Obj) β†’ Hom x x
    _∘_ : {x y z : Obj} β†’ Hom y z β†’ Hom x y β†’ Hom x z
    refl : {x y : Obj} (f : Hom x y) β†’ f β‰ˆ f
    sym : {x y : Obj} {f g : Hom x y} β†’ f β‰ˆ g β†’ g β‰ˆ f
    trans : {x y : Obj} {f g h : Hom x y} β†’ g β‰ˆ h β†’ f β‰ˆ g β†’ f β‰ˆ h
    congr : {x y z : Obj} {g gβ€² : Hom y z} {f fβ€² : Hom x y}
      β†’ g β‰ˆ gβ€² β†’ f β‰ˆ fβ€² β†’ (g ∘ f) β‰ˆ (gβ€² ∘ fβ€²)

record Laws {o h p : Level} (C : Composition o h p) : Set (o βŠ” h βŠ” p) where
  open Composition C
  field
    assoc : {w x y z : Obj} (h : Hom y z) (g : Hom x y) (f : Hom w x)
      β†’ ((h ∘ g) ∘ f) β‰ˆ (h ∘ (g ∘ f))
    unitΛ‘ : {x y : Obj} (f : Hom x y) β†’ (id y ∘ f) β‰ˆ f
    unitΚ³ : {x y : Obj} (f : Hom x y) β†’ (f ∘ id x) β‰ˆ f
```

Cancellation needs only the displayed inverse comparison. It does not
require an inverse operation or a global choice of inverses. Reassociate,
apply that comparison, and remove the identity.

```agda
module Calculation {o h p : Level} (C : Composition o h p) (L : Laws C) where
  open Composition C
  open Laws L

  abstract
    cancel-left : {x y z : Obj} (r : Hom z y) (s : Hom y z) (f : Hom x y)
      β†’ (r ∘ s) β‰ˆ id y β†’ (r ∘ (s ∘ f)) β‰ˆ f
    cancel-left r s f inverse =
      trans (unitΛ‘ f) (trans (congr inverse (refl f)) (sym (assoc r s f)))

    cancel-right : {x y z : Obj} (f : Hom y z) (s : Hom x y) (r : Hom y x)
      β†’ (s ∘ r) β‰ˆ id y β†’ ((f ∘ s) ∘ r) β‰ˆ f
    cancel-right f s r inverse =
      trans (unitΚ³ f) (trans (congr (refl f) inverse) (assoc f s r))

    reassociate-four : {v w x y z : Obj}
      (k : Hom y z) (h : Hom x y) (g : Hom w x) (f : Hom v w)
      β†’ (((k ∘ h) ∘ g) ∘ f) β‰ˆ (k ∘ (h ∘ (g ∘ f)))
    reassociate-four k h g f =
      trans (assoc k h (g ∘ f)) (assoc (k ∘ h) g f)
```