module Cat.Restriction.Instances.Allegory where

Restriction Categories from AllegoriesπŸ”—

Let A\mathcal{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.

  Partial-maps-subcat : Wide-subcat {C = 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-∘ f-partial g-partial =
    functional-∘ f-partial g-partial

  Partial-maps : Precategory o (β„“ βŠ” β„“')
  Partial-maps = Wide Partial-maps-subcat

This category can be equipped with a restriction structure, defining f↓f^{\downarrow} 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 =
    Wide-hom-path $ domain-absorb (f .hom)
  Partial-maps-restriction .↓-comm f g =
    Wide-hom-path $ domain-comm
  Partial-maps-restriction .↓-smashr f g =
    Wide-hom-path $ domain-smashr (g .hom) (f .hom)
  Partial-maps-restriction .↓-swap f g =
    Wide-hom-path $ domain-swap (f .hom) (g .hom) (g .witness)