module Cat.Restriction.Instances.Allegory where

# Restriction categories from allegoriesπ

Let
$A$
be an allegory, considered as a
sort of generalized category of βsets and relationsβ. Much like we can
recover a category of βsets and functionsβ via the associated category of maps, we can recover a
category of βsets and partial functionsβ by only restricting to functional
relations instead of functional *and* entire
relations.

module _ {o β β'} (A : Allegory o β β') where open Cat.Allegory.Morphism A open Restriction-category open Wide-hom

Partial-maps-subcat : Wide-subcat cat β' Partial-maps-subcat .Wide-subcat.P = is-functional Partial-maps-subcat .Wide-subcat.P-prop f = β€-thin Partial-maps-subcat .Wide-subcat.P-id = functional-id Partial-maps-subcat .Wide-subcat.P-β = functional-β Partial-maps : Precategory o (β β β') Partial-maps = Wide Partial-maps-subcat

This category can be equipped with a restriction structure, defining $f_{β}$ to be the domain of the partial maps. Note that the first 3 axioms donβt actually require the relation to be functional; itβs only relevant in the converse direction of the 4th axiom!

Partial-maps-restriction : Restriction-category Partial-maps Partial-maps-restriction ._β f .hom = domain (f .hom) Partial-maps-restriction ._β f .witness = domain-functional (f .hom) Partial-maps-restriction .β-dom f = ext $ domain-absorb (f .hom) Partial-maps-restriction .β-comm f g = ext domain-comm Partial-maps-restriction .β-smashr f g = ext $ domain-smashr (g .hom) (f .hom) Partial-maps-restriction .β-swap f g = ext $ domain-swap (f .hom) (g .hom) (g .witness)