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

Monads in Spans(Sets)🔗

Let be a strict category. Whatever your favourite strict category might be — it doesn’t matter in this case. Let denote its set of objects, and write for its Hom-family. We know that families are equivalently fibrations, so that we may define

and, since the family is valued in and indexed by a set, so is We can picture 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 and yields a morphism, i.e. something in 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 in the bicategory

Phrased like this, we see that the composition map gives an associative and unital procedure for mapping 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)
  module C = Precategory C

  homs : Span (Sets ℓ) (el _ cset) (el _ cset)
  homs .apex = el (Σ[ x ∈ C ] Σ[ y ∈ C ] (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 We omit the verification here and instruct the curious reader to check the proof on GitHub.

  m .ÎŒ-assoc = Span-hom-path (Sets ℓ) $ funext λ where
    ((w , x , f) , ((y , z , g) , (a , b , h) , p) , q) →
      J' (λ w z q → ∀ (f : C.Hom w x) {y b} (p : y ≡ b) (g : C .Hom y z)
                      (h : C.Hom a b)
                  → (mult Sb.∘ (homs Sb.▶ mult)) .map ((w , x , f) , ((y , z , g) , (a , b , h) , p) , q)
                  ≡ (mult Sb.∘ (mult Sb.◀ homs) Sb.∘ Sb.α← homs homs homs) .map ((w , x , f) , ((y , z , g) , (a , b , h) , p) , q))
         (λ w f → J' (λ y b p → (g : C.Hom y w) (h : C.Hom a b) →
            (mult Sb.∘ (homs Sb.▶ mult)) .map ((w , x , f) , ((y , w , g) , (a , b , h) , p) , refl)
          ≡ (mult Sb.∘ (mult Sb.◀ homs) Sb.∘ Sb.α← homs homs homs) .map ((w , x , f) , ((y , w , g) , (a , b , h) , p) , refl))
          λ y g h → Σ-pathp refl (Σ-pathp refl (C.assoc _ _ _
            ∙ ap₂ C._∘_ (ap₂ C._∘_ (ap (λ p → subst (λ e → C.Hom e x) p f) (hlevel 2 w w _ refl) ∙ transport-refl _)
                                   (ap (λ p → subst (λ e → C.Hom e w) p g) (hlevel 2 y y _ refl) ∙ transport-refl _)
                        ∙ sym ((ap (subst (λ e → C.Hom e x) _)
                                  (ap₂ C._∘_ ((ap (λ p → subst (λ e → C.Hom e x) p f) (hlevel 2 w w _ refl) ∙ transport-refl _))
                                  refl) ∙ ap (λ p → subst (λ e → C.Hom e x) p (f C.∘ g)) (hlevel 2 y y _ refl) ∙ transport-refl _)))
                        refl)))
         q f p g h
  m .ÎŒ-unitr = Span-hom-path (Sets ℓ) $ funext λ where
    ((x , y , f) , z , p) →
      J' (λ x z p → (f : C .Hom x y) → (mult Sb.∘ (homs Sb.▶ unit)) .map ((x , y , f) , z , p)
                                     ≡ (x , y , f))
         (λ x f → Σ-pathp refl
            (Σ-pathp refl (ap₂ C._∘_ (ap (λ p → subst (λ e → C.Hom e y) p f) (hlevel 2 _ _ _ _) ∙ transport-refl _) refl
                          ∙ C.idr _)))
         p f
  m .ÎŒ-unitl = Span-hom-path (Sets ℓ) $ funext λ where
    (x , (y , z , f) , p) →
      J' (λ x z p → (f : C .Hom y z)
           → (mult Sb.∘ (unit Sb.◀ homs)) .map (x , (y , z , f) , p)
           ≡ (y , z , f))
         (λ x f → Σ-pathp refl
            (Σ-pathp refl (ap₂ C._∘_ (ap (λ p → subst (λ e → C.Hom e x) p C.id) (hlevel 2 _ _ _ _) ∙ transport-refl _) refl
                          ∙ C.idl _)))
         p f

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 ] ((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 of our recovered category is precisely the fibre of over the pair The commutativity conditions for 2-cells in implies that source and target are preserved through composition, and that the identity morphism — that is, the image of under the unit map — lies in the fibre over

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!
    ( ap (Ό .map) (ap (f .fst ,_) (Σ-prop-path! refl))
    ∙ happly (ap map ÎŒ-unitr) (f .fst , x , f .snd .fst))
  precat .idl {x} {y} f = Σ-prop-path!
    ( ap (Ό .map) (ap (η .map y ,_) (Σ-prop-path! refl))
    ∙ happly (ap map ÎŒ-unitl) (y , f .fst , sym (f .snd .snd)))
  precat .assoc f g h = Σ-prop-path!
    ( ap (Ό .map) (ap (f .fst ,_) (Σ-prop-path!
        (ap (Ό .map) (ap (g .fst ,_)
          (Σ-prop-path! (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! refl)))
           (Σ-pathp refl (is-prop→pathp (λ _ → hlevel 1) _ _))))