open import Cat.Prelude

module Cat.Restriction.Base where

Restriction categories🔗

Much of computer science involves the study of partial functions. Unfortunately, partial functions are somewhat tedious to work with, as they aren’t really functions; they’re relations! Furthermore, we are often interested in computable partial functions; this means that we can not identify partial functions $A\rightharpoonup B$ with total functions $A\to \mathrm{Maybe}(B)$¹. This leaves us with a few possible approaches. The most first approach that may come to mind is to encode partial functions $A\rightharpoonup B$ as total functions from a subobject $X\hookrightarrow A\text{.}$ Alternatively, we could find some construction that classifies partial maps; this is what the naive Maybe approach attempted to do. We could also just work with functional relations directly, though this is ill-advised.

Each of these approaches has its own benefits and drawbacks, which makes choosing one difficult. Restriction categories offer an alternative, algebraic approach to the problem, allowing us to neatly sidestep any questions about encodings.

Our prototypical restriction category will be $\mathbf{Par}\text{,}$ the category of sets and partial functions. The key insight is that every partial function $f:A\rightharpoonup B$ is defined on some domain $X\subseteq A\text{;}$ this yields a partial function $f\downarrow :A\rightharpoonup A$ that maps $x$ to itself iff $f(x)$ is defined. We can generalize this insight to an arbitrary category $\mathcal{C}$ by equipping $\mathcal{C}$ with an operation $(-{)}^{\downarrow }:\mathcal{C}(x,y)\to \mathcal{C}(x,x)\text{.}$

–

record Restriction-category
  {o ℓ} (C : Precategory o ℓ)
  : Type (o ⊔ ℓ) where
  no-eta-equality
  open Precategory C
  field
    _↓ : ∀ {x y} → Hom x y → Hom x x

  infix  _↓

We require that $(-{)}^{\downarrow }$ satisfies 4 axioms: - $f{f}^{\downarrow }=f\text{.}$ In $\mathbf{Par}\text{,}$ this corresponds to the fact that $f^{\downarrow }(x)$ is defined to be $x$ iff $f$ is defined, so precomposing with it does nothing.

  field
    ↓-dom : ∀ {x y} → (f : Hom x y) → f ∘ (f ↓) ≡ f

• $f^{\downarrow }{g}^{\downarrow }=g^{\downarrow }{f}^{\downarrow }\text{.}$ In $\mathbf{Par}\text{,}$ this falls out of the fact that restriction maps do not modify their arguments, and it doesn’t matter if $f$ diverges first or $g$ does; all that matters is that it diverges!

  field
    ↓-comm : ∀ {x y z} → (f : Hom x z) (g : Hom x y) → f ↓ ∘ g ↓ ≡ g ↓ ∘ f ↓

• $(g{f}^{\downarrow }{)}^{\downarrow }=g^{\downarrow }{f}^{\downarrow }\text{.}$ This axiom holds in the $\mathbf{Par}\text{,}$ as $(g{f}^{\downarrow }{)}^{\downarrow }(x)$ ignores the action of $g$ on $x\text{,}$ and focuses only on its termination.

  field
    ↓-smashr : ∀ {x y z} → (f : Hom x z) (g : Hom x y) → (g ∘ f ↓) ↓ ≡ g ↓ ∘ f ↓

• $f^{\downarrow }g=g(fg{)}^{\downarrow }\text{.}$ This is the trickiest of the bunch to understand in $\mathbf{Par}\text{.}$ Note that if we postcompose $g$ with a domain map $f^{\downarrow }\text{,}$ then we still need to take into account the action of $g\text{;}$ furthermore, its domain of definition needs to be restricted to image of $g\text{.}$

  field
    ↓-swap : ∀ {x y z} → (f : Hom y z) (g : Hom x y) → f ↓ ∘ g ≡ g ∘ (f ∘ g) ↓