{-# OPTIONS --lossy-unification -vtc.def.fun:10 #-}
open import Cat.Instances.Sets.Complete
open import Cat.Bi.Instances.Spans
open import Cat.Bi.Diagram.Monad
open import Cat.Instances.Sets
open import Cat.Bi.Base
open import Cat.Prelude

module Cat.Bi.Diagram.Monad.Spans {ℓ} where

Monads in Spans(Sets)🔗

Let $\mathcal{C}$ be a strict category. Whatever your favourite strict category might be — it doesn’t matter in this case. Let $\mathcal{C}_0$ denote its set of objects, and write $\mathcal{C}(x, y)$ for its Hom-family. We know that families are equivalently fibrations, so that we may define

$\mathcal{C}_1 = \sum_{x, y : \mathcal{C}_0} \mathcal{C}(x, y)\text{,}$

and, since the family is valued in ${{\mathbf{Sets}}}$ and indexed by a set, so is $\mathcal{C}_1$ . We can picture $\mathcal{C}_1$ together with the components of its first projection as a span in the category of sets

Under this presentation, what does the composition operation correspond to? Well, it takes something in the object of composable morphisms, a certain subset of $\mathcal{C}_1 \times \mathcal{C}_1$ , and yields a morphism, i.e. something in $\mathcal{C}_1$ . Moreover, this commutes with taking source/target: The source of the composition is the source of its first argument, and the target is the target of its second argument. The key observation, that will lead to a new representation of categories, is that the object of composable morphisms is precisely the composition $\mathcal{C}_1 \circ \mathcal{C}_1$ in the bicategory ${\mathbf{Span}}({{\mathbf{Sets}}})$ !

Phrased like this, we see that the composition map gives an associative and unital procedure for mapping $(\mathcal{C}_1\mathcal{C}_1) {\Rightarrow}\mathcal{C}_1$ in a certain bicategory — a monad in that bicategory.

Spans[Sets] : Prebicategory _ _ _
Spans[Sets] = Spanᵇ (Sets ℓ) Sets-pullbacks

strict-category→span-monad
  : (C : Precategory ℓ ℓ) (cset : is-set (C .Ob))
  → Monad Spans[Sets] (el _ cset)
strict-category→span-monad C cset = m where
  open Monad
  open n-Type (el {n = 2} _ cset) using (H-Level-n-type)
  open Precategory.HLevel-instance C
  module C = Precategory C

  homs : Span (Sets ℓ) (el _ cset) (el _ cset)
  homs .apex = el (Σ[ x ∈ C .Ob ] Σ[ y ∈ C .Ob ] (C .Hom x y)) (hlevel 2)
  homs .left (x , _ , _) = x
  homs .right (_ , y , _) = y

  mult : _ Sb.⇒ _
  mult .map ((x , y , f) , (z , x′ , g) , p) =
    z , y , subst (λ e → C.Hom e y) p f C.∘ g
  mult .left = refl
  mult .right = refl

  unit : _ Sb.⇒ _
  unit .map x = x , x , C .id
  unit .left = refl
  unit .right = refl

  m : Monad Spans[Sets] (el (C .Ob) cset)
  m .M = homs
  m .μ = mult
  m .η = unit

It is annoying, but entirely straightforward, to verify that the operations mult and unit defined above do constitute a monad in ${\mathbf{Span}}({{\mathbf{Sets}}})$ . We omit the verification here and instruct the curious reader to check the proof on GitHub.

Conversely, if we have an associative and unital method mapping composable morphisms into morphisms, it stands to reason that we should be able to recover a category. Indeed, we can! The verification is once more annoying, but unsurprising. Since it’s less of a nightmare this time around, we include it in full below.

span-monad→strict-category : ∀ (C : Set ℓ) → Monad Spans[Sets] C → Precategory _ _
span-monad→strict-category C monad = precat where
  open Monad monad

  open n-Type C using (H-Level-n-type)
  open n-Type (M .apex) using (H-Level-n-type)

  precat : Precategory _ _
  precat .Ob = ∣ C ∣
  precat .Hom a b = Σ[ s ∈ ∣ M .apex ∣ ] ((M .left s ≡ a) × (M .right s ≡ b))
  precat .Hom-set x y = hlevel 2
  precat .id {x} = η .map x , sym (happly (η .left) x) , sym (happly (η .right) x)
  precat ._∘_ (f , fs , ft) (g , gs , gt) =
      μ .map (f , g , fs ∙ sym gt)
    , sym (happly (μ .left) _) ∙ gs
    , sym (happly (μ .right) _) ∙ ft

The family of morphisms ${\mathbf{Hom}}(x,y)$ of our recovered category is precisely the fibre of $(s,t) : \mathcal{C}_1 \to \mathcal{C}_0 \times \mathcal{C}_0$ over the pair $x, y$ . The commutativity conditions for 2-cells in ${\mathbf{Span}}({{\mathbf{Sets}}})$ implies that source and target are preserved through composition, and that the identity morphism — that is, the image of $x$ under the unit map — lies in the fibre over $x, x$ .

The verification follows from the monad laws, and it would be trivial in extensional type theory, but the tradeoff for decidable type-checking is having to munge paths sometimes. This is one of those times:

  precat .idr {x} {y} f = Σ-prop-path (λ _ → hlevel 1)
    ( ap (μ .map) (ap (f .fst ,_) (Σ-prop-path (λ _ → C .is-tr _ _) refl))
    ∙ happly (ap map μ-unitr) (f .fst , x , f .snd .fst))
  precat .idl {x} {y} f = Σ-prop-path (λ _ → hlevel 1)
    ( ap (μ .map) (ap (η .map y ,_) (Σ-prop-path (λ _ → C .is-tr _ _) refl))
    ∙ happly (ap map μ-unitl) (y , f .fst , sym (f .snd .snd)))
  precat .assoc f g h = Σ-prop-path (λ _ → hlevel 1)
    ( ap (μ .map) (ap (f .fst ,_) (Σ-prop-path (λ _ → hlevel 1)
        (ap (μ .map) (ap (g .fst ,_)
          (Σ-prop-path (λ _ → hlevel 1) (refl {x = h .fst}))))))
    ·· happly (ap map μ-assoc)
        ( f .fst , (g .fst , h .fst , g .snd .fst ∙ sym (h .snd .snd))
        , f .snd .fst ∙ sym (g .snd .snd)
        )
    ·· ap (μ .map) (Σ-pathp (ap (μ .map) (ap (f .fst ,_)
        (Σ-prop-path (λ _ → hlevel 1) refl)))
           (Σ-pathp-dep refl (is-prop→pathp (λ _ → hlevel 1) _ _))))