open import Cat.Allegory.Base
open import Cat.Prelude

import Cat.Allegory.Reasoning as Ar

module Cat.Allegory.Maps where


# Maps in allegoriesπ

Suppose we have an allegory $\mathcal{A}$ β for definiteness you could consider the archetypal allegory $\mathbf{Rel}$ β 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 $\mathbf{Rel}$!

If you have a relation $R \hookrightarrow A \times B$, when does it correspond to a function $A \to B$? Well, it must definitely be functional: if we want $R(x, y)$ to represent β$f(x) = y$β, then surely if $R(x, y) \land R(x, z)$, we must have $y = z$. In allegorical language, we would say $RR^o \le \mathrm{id}_{}$, which we can calculate to mean (in $\mathbf{Rel}$) that, for all $x, y$,

$(\exists z, R(z, x) \land R(z, y)) \to (x = y)\text{.}$

It must also be an entire relation: Every $x$ must at least one $y$ it is related to, and by functionality, exactly one $y$ it is related to. This is the βvalue ofβ the function at $y$.

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 $a$ in the domain) the space of βpoints in the codomain related to $a$β 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 $\mathcal{A}$, we can form a category $\mathrm{Map}(\mathcal{A})$ with the same objects as $\mathcal{A}$, 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 $f \dashv f^o$, 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 _ _ _)