module Cat.Allegory.Maps where
Maps in allegoriesπ
Suppose we have an allegory β for definiteness you could consider the archetypal allegory β but what we really wanted was to get our hands on an ordinary category. That is: we want, given some category of βsets and relationsβ, to recover the associated category of βsets and functionsβ. So, letβs start by thinking about !
If you have a relation , when does it correspond to a function ? Well, it must definitely be functional: if we want to represent ββ, then surely if , we must have . In allegorical language, we would say , which we can calculate to mean (in ) that, for all ,
It must also be an entire relation: Every must at least one it is related to, and by functionality, exactly one it is related to. This is the βvalue ofβ the function at .
module _ {o β h} (A : Allegory o β h) where open Allegory A record is-map x y (f : Hom x y) : Type h where constructor mapping field functional : f β f β β€ id entire : id β€ f β β f module _ {o β h} {A : Allegory o β h} where open Allegory A open is-map instance H-Level-is-map : β {x y} {f : Hom x y} {n} β H-Level (is-map A x y f) (suc n) H-Level-is-map = prop-instance {T = is-map A _ _ _} Ξ» where x y i .functional β β€-thin (x .functional) (y .functional) i x y i .entire β β€-thin (x .entire) (y .entire) i
We can calculate that a functional entire relation is precisely a function between sets: Functionality ensures that (fixing a point in the domain) the space of βpoints in the codomain related to β is a subsingleton, and entireness ensures that it is inhabited; By unique choice, we can project the value of the function.
Rel-mapβfunction : β {β} {x y : Set β} {f : Allegory.Hom (Rel β) x y} β is-map (Rel β) x y f β β£ x β£ β β£ y β£ Rel-mapβfunction {x = x} {y} {rel} map elt = β₯-β₯-rec {P = Ξ£ β£ y β£ Ξ» b β β£ rel elt b β£} (Ξ» { (x , p) (y , q) β Ξ£-prop-path (Ξ» _ β hlevel!) (functionalβ² p q) }) (Ξ» x β x) (entireβ² elt) .fst where module map = is-map map functionalβ² : β {a b c} β β£ rel a b β£ β β£ rel a c β£ β b β‘ c functionalβ² r1 r2 = out! (map.functional _ _ (inc (_ , r1 , r2))) entireβ² : β a β β β£ y β£ Ξ» b β β£ rel a b β£ entireβ² a = β‘-rec! (Ξ» { (x , y , R) β inc (x , R) }) (map.entire a a (inc refl))
The category of mapsπ
Given an allegory , we can form a category with the same objects as , but considering only the maps (rather than arbitrary relations).
module _ {o β h} (A : Allegory o β h) where private module A = Ar A open is-map open Precategory hiding (_β_ ; id) open A using (_β ; _β_ ; id ; _β_ ; _βΆ_) Maps[_] : Precategory _ _ Maps[_] .Ob = A.Ob Maps[_] .Hom x y = Ξ£ (A.Hom x y) (is-map A x y) Maps[_] .Hom-set x y = hlevel 2
Proving that maps compose is a bit annoying, but it follows from the properties of the duality involution. By the way: This is essentially the proof that adjunctions compose! This is because, sneakily, the property βbeing a mapβ is defined to be , but without using those words.
Maps[_] .Precategory.id = A.id , mapping (subst (A._β€ id) (sym (A.idl _ β dual-id A)) A.β€-refl) (subst (id A.β€_) (sym (A.idr _ β dual-id A)) A.β€-refl) Maps[_] .Precategory._β_ (f , m) (g , mβ²) = f A.β g , mapping ( (f β g) β (f β g) β A.=β¨ A.β -inner refl β©A.= f β (g β g β ) β f β A.β€β¨ f βΆ mβ² .functional β f β β©A.β€ f β id β f β A.=β¨ A.reflβ©ββ¨ A.idl _ β©A.= f β f β A.β€β¨ m .functional β©A.β€ id A.β€β ) ( id A.β€β¨ mβ² .entire β©A.β€ g β β g A.=β¨ ap (g β β_) (sym (A.idl _)) β©A.= g β β id β g A.β€β¨ g β βΆ m .entire β g β©A.β€ g β β (f β β f) β g A.=β¨ A.pulll (A.pulll (sym A.dual-β)) β A.pullr refl β©A.= (f β g) β β (f β g) A.β€β ) Maps[_] .idr f = Ξ£-prop-path (Ξ» _ β hlevel 1) (A.idr _) Maps[_] .idl f = Ξ£-prop-path (Ξ» _ β hlevel 1) (A.idl _) Maps[_] .assoc f g h = Ξ£-prop-path (Ξ» _ β hlevel 1) (A.assoc _ _ _)