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 with total functions 1. This leaves us with a few possible approaches. The most first approach that may come to mind is to encode partial functions as total functions from a subobject 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 the category of sets and partial functions. The key insight is that every partial function is defined on some domain this yields a partial function that maps to itself iff is defined. We can generalize this insight to an arbitrary category by equipping with an operation

β

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 50 _β


We require that satisfies 4 axioms: - In this corresponds to the fact that is defined to be iff is defined, so precomposing with it does nothing.

  field
β-dom : β {x y} β (f : Hom x y) β f β (f β) β‘ f

• In this falls out of the fact that restriction maps do not modify their arguments, and it doesnβt matter if diverges first or 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 β

• This axiom holds in the as ignores the action of on and focuses only on its termination.
  field
β-smashr : β {x y z} β (f : Hom x z) (g : Hom x y) β (g β f β) β β‘ g β β f β

• This is the trickiest of the bunch to understand in Note that if we postcompose with a domain map then we still need to take into account the action of furthermore, its domain of definition needs to be restricted to image of
  field
β-swap : β {x y z} β (f : Hom y z) (g : Hom x y) β f β β g β‘ g β (f β g) β


1. We can easily determine if functions into Maybe βdivergeβ by checking if they return nothing. If we identify partial functions with total functions into Maybe, we can decide if a partial function terminates, which is extremely uncomputable!β©οΈ