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



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

: (C : Precategory ℓ ℓ) (cset : is-set (C .Ob))
→ Monad Spans[Sets] (el _ cset)
strict-category→span-monad C cset = m where
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 _ _

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) _ _))))