open import Cat.Functor.WideSubcategory
open import Cat.Restriction.Base
open import Cat.Allegory.Base
open import Cat.Prelude

import Cat.Allegory.Morphism

module Cat.Restriction.Instances.Allegory where


# Restriction categories from allegoriesπ

Let 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 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)