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 A\mathcal{A} β€” for definiteness you could consider the archetypal allegory Rel{{\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 Rel{{\mathbf{Rel}}}!

If you have a relation Rβ†ͺAΓ—BR {\hookrightarrow}A \times B, when does it correspond to a function Aβ†’BA \to B? Well, it must definitely be functional: if we want R(x,y)R(x, y) to represent β€œf(x)=yf(x) = y”, then surely if R(x,y)∧R(x,z)R(x, y) \land R(x, z), we must have y=zy = z. In allegorical language, we would say RRo≀idRR^o \le {{\mathrm{id}}_{}}, which we can calculate to mean (in Rel{{\mathbf{Rel}}}) that, for all x,yx, y,

(βˆƒz,R(z,x)∧R(z,y))β†’(x=y). (\exists z, R(z, x) \land R(z, y)) \to (x = y)\text{.}

It must also be an entire relation: Every xx must at least one yy it is related to, and by functionality, exactly one yy it is related to. This is the β€œvalue of” the function at yy.

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 aa in the domain) the space of β€œpoints in the codomain related to aa” 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 A\mathcal{A}, we can form a category Map(A){\mathrm{Map}}(\mathcal{A}) with the same objects as A\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⊣fof \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 _ _ _)