module Cat.Bi.Instances.Spans {o β„“} (C : Precategory o β„“) where

The bicategory of spansπŸ”—

Let C\mathcal{C} be a precategory. By a span in C\mathcal{C} (from an object A:CA : \mathcal{C} to an object B:CB : \mathcal{C}), we mean a diagram of the form A←Cβ†’BA \leftarrow C \to B. Note that the β€œvertex” of this span, the object CC, is part of the data, so that the collection of β€œspans in C\mathcal{C}” will not be a set (unless C\mathcal{C} is strict) β€” so we can not construct a category where Hom(a,b)\mathbf{Hom}(a,b) is the collection of spans from aa to bb.

However, we can make spans in C\mathcal{C} the objects of a category, and the hom-sets are the maps in C\mathcal{C} between the vertices which β€œcommute with the legs”. Diagramatically, a map between spans is the dashed line in

where both the left and right triangles must commute.

record Span (a b : Ob) : Type (o βŠ” β„“) where
  constructor span
  field
    apex  : Ob
    left  : Hom apex a
    right : Hom apex b

open Span

record Span-hom {a b : Ob} (x y : Span a b) : Type β„“ where
  no-eta-equality
  field
    map   : Hom (x .apex) (y .apex)
    left  : x .left  ≑ y .left ∘ map
    right : x .right ≑ y .right ∘ map

The category Spans⁑C(A,B)\operatorname{Spans}_\mathcal{C}(A, B) of spans between AA and BB admits a faithful functor to C\mathcal{C} (projecting the vertex and the β€œmiddle map”, respectively), so that equality of maps of spans can be compared at the level of maps in C\mathcal{C}.

Spans : Ob β†’ Ob β†’ Precategory _ _
Spans x y .Precategory.Ob = Span x y
Spans x y .Precategory.Hom = Span-hom
Spans x y .Precategory.Hom-set _ _ = Iso→is-hlevel 2 eqv (hlevel 2)
Spans x y .Precategory.id .map = id
Spans x y .Precategory.id .left = intror refl
Spans x y .Precategory.id .right = intror refl
Spans x y .Precategory._∘_ f g .map = f .map ∘ g .map
Spans x y .Precategory._∘_ f g .left = g .left βˆ™ pushl (f .left)
Spans x y .Precategory._∘_ f g .right = g .right βˆ™ pushl (f .right)
Spans x y .Precategory.idr f = Span-hom-path (idr _)
Spans x y .Precategory.idl f = Span-hom-path (idl _)
Spans x y .Precategory.assoc f g h = Span-hom-path (assoc _ _ _)

Now suppose that C\mathcal{C} admits pullbacks for arbitrary pairs of maps. Supposing that we have some spans S:A→BS : A \to B and S′:B→CS' : B \to C, we can fit them in an M-shaped diagram like

so that taking the pullback of the diagram Sβ†’B←Sβ€²S \to B \leftarrow S' gives us an universal solution to the problem of finding a span A←(SΓ—BSβ€²)β†’CA \leftarrow (S \times_B S') \to C. Since pullbacks are universal, this composition operation is functorial, and so extends to a composition operation Span-∘:

module _ (pb : βˆ€ {a b c} (f : Hom a b) (g : Hom c b) β†’ Pullback C f g) where
  open Functor

  Span-∘ : βˆ€ {a b c} β†’ Functor (Spans b c Γ—αΆœ Spans a b) (Spans a c)
  Span-∘ .Fβ‚€ (sp1 , sp2) =
    span pb.apex (sp2 .left ∘ pb.pβ‚‚) (sp1 .right ∘ pb.p₁)
    where module pb = Pullback (pb (sp1 .left) (sp2 .right))

  Span-∘ .F₁ {x1 , x2} {y1 , y2} (f , g) = res
    where
      module x = Pullback (pb (x1 .left) (x2 .right))
      module y = Pullback (pb (y1 .left) (y2 .right))

      x→y : Hom x.apex y.apex
      xβ†’y = y.universal {p₁' = f .map ∘ x.p₁} {pβ‚‚' = g .map ∘ x.pβ‚‚} comm
        where abstract
          open Pullback
          comm : y1 .left ∘ f .map ∘ x.p₁ ≑ y2 .right ∘ g .map ∘ x.pβ‚‚
          comm = pulll (sym (f .left)) βˆ™ x.square βˆ™ pushl (g .right)

      res : Span-hom _ _
      res .map = x→y
      res .left = sym (pullr y.pβ‚‚βˆ˜universal βˆ™ pulll (sym (g .left)))
      res .right = sym (pullr y.pβ‚βˆ˜universal βˆ™ pulll (sym (f .right)))

  Span-∘ .F-id {x1 , x2} = Span-hom-path $ sym $ x.unique id-comm id-comm
    where module x = Pullback (pb (x1 .left) (x2 .right))

  Span-∘ .F-∘ {x1 , x2} {y1 , y2} {z1 , z2} f g =
    Span-hom-path $ sym $ z.unique
      (pulll z.pβ‚βˆ˜universal βˆ™ pullr y.pβ‚βˆ˜universal βˆ™ assoc _ _ _)
      (pulll z.pβ‚‚βˆ˜universal βˆ™ pullr y.pβ‚‚βˆ˜universal βˆ™ assoc _ _ _)
    where
      module x = Pullback (pb (x1 .left) (x2 .right))
      module y = Pullback (pb (y1 .left) (y2 .right))
      module z = Pullback (pb (z1 .left) (z2 .right))

What we’ll show in the rest of this module is that Span-∘ lets us make Spans into the categories of 1-cells of a prebicategory, the (pre)bicategory of spans (of C\mathcal{C}), Spans⁑(C)\operatorname{Spans}(\mathcal{C}). As mentioned before, this prebicategory has (a priori) no upper bound on the h-levels of its 1-cells, so it is not locally strict. We remark that when C\mathcal{C} is univalent, then Spans⁑(C)\operatorname{Spans}(\mathcal{C}) is locally so, and when C\mathcal{C} is gaunt, then Spans⁑(C)\operatorname{Spans}(\mathcal{C}) is strict.

Since the details of the full construction are grueling, we will present only an overview of the unitors and the associator. For the left unitor, observe that the composition id⁑∘S\operatorname{id}_{} \circ S is implemented by a pullback diagram like

but observe that the maps Sβ†’fAS \xrightarrow{f} A and Sβ†’id⁑SS \xrightarrow{\operatorname{id}_{}} S also form a cone over the cospan Aβ†’A←fSA \to A \xleftarrow{f} S, so that there is a unique map filling the dashed line in the diagram above such that everything commutes: hence there is an invertible 2-cell id⁑∘Sβ‡’S\operatorname{id}_{} \circ S \Rightarrow S. The right unitor is analogous.

  open Prebicategory
  open Pullback

  private
    _Β€_ : βˆ€ {a b c} (x : Span b c) (y : Span a b) β†’ Span a c
    f Β€ g = Span-∘ .Fβ‚€ (f , g)

    sλ← : βˆ€ {A B} (x : Span A B) β†’ Span-hom x (span _ C.id C.id Β€ x)
    sλ← x .map   = pb _ _ .universal id-comm-sym
    sλ← x .left  = sym $ pullr (pb _ _ .pβ‚‚βˆ˜universal) βˆ™ idr _
    sλ← x .right = sym $ pullr (pb _ _ .pβ‚βˆ˜universal) βˆ™ idl _

    sρ← : βˆ€ {A B} (x : Span A B) β†’ Span-hom x (x Β€ span _ C.id C.id)
    sρ← x .map   = pb _ _ .universal id-comm
    sρ← x .left  = sym $ pullr (pb _ _ .pβ‚‚βˆ˜universal) βˆ™ idl _
    sρ← x .right = sym $ pullr (pb _ _ .pβ‚βˆ˜universal) βˆ™ idr _

For the associator, while doing the construction in elementary terms is quite complicated, we observe that, diagramatically, the composite of three morphisms fits into a diagram like

so that, at a high level, there is no confusion as to which composite is meant. From then, it’s just a matter of proving pullbacks are associative (in a standard, but annoying, way), and showing that these canonically-obtained isomorphisms (are natural in all the possible variables and) satisfy the triangle and pentagon identities.

On second thought, let’s not read that. T’is a silly theorem.
    sα← : βˆ€ {A B C D} ((f , g , h) : Span C D Γ— Span B C Γ— Span A B)
        β†’ Span-hom ((f Β€ g) Β€ h) (f Β€ (g Β€ h))
    sα← (f , g , h) .map = pb _ _ .universal respβ€² where
      abstract
        resp : g .left C.∘ pb (f .left) (g .right) .pβ‚‚
           C.∘ pb ((f Β€ g) .left) (h .right) .p₁
             ≑ h .right C.∘ pb ((f Β€ g) .left) (h .right) .pβ‚‚
        resp = assoc _ _ _ βˆ™ pb _ _ .square

      shuffle = pb _ _ .universal {p₁' = pb _ _ .pβ‚‚ C.∘ pb _ _ .p₁} {pβ‚‚' = pb _ _ .pβ‚‚} resp

      abstract
        respβ€² : f .left C.∘ pb (f .left) (g .right) .p₁
            C.∘ pb ((f Β€ g) .left) (h .right) .p₁
              ≑ (g Β€ h) .right C.∘ shuffle
        respβ€² = sym $ pullr (pb _ _ .pβ‚βˆ˜universal) βˆ™ extendl (sym (pb _ _ .square))

    sα← (f , g , h) .left = sym $ pullr (pb _ _ .pβ‚‚βˆ˜universal) βˆ™ pullr (pb _ _ .pβ‚‚βˆ˜universal)
    sα← (f , g , h) .right = sym $ pullr (pb _ _ .pβ‚βˆ˜universal) βˆ™ assoc _ _ _

    sΞ±β†’ : βˆ€ {A B C D} ((f , g , h) : Span C D Γ— Span B C Γ— Span A B)
        β†’ Span-hom (f Β€ (g Β€ h)) ((f Β€ g) Β€ h)
    sΞ±β†’ (f , g , h) .map = pb _ _ .universal respβ€² where
      abstract
        resp : f .left C.∘ pb (f .left) ((g Β€ h) .right) .p₁
             ≑ g .right C.∘ pb (g .left) (h .right) .p₁
           C.∘ pb (f .left) ((g Β€ h) .right) .pβ‚‚
        resp = pb _ _ .square βˆ™ sym (assoc _ _ _)

      shuffle = pb _ _ .universal {p₁' = pb _ _ .p₁} {pβ‚‚' = pb _ _ .p₁ C.∘ pb _ _ .pβ‚‚} resp

      abstract
        respβ€² : (f Β€ g) .left C.∘ shuffle
              ≑ h .right C.∘ pb (g .left) (h .right) .pβ‚‚
            C.∘ pb (f .left) ((g Β€ h) .right) .pβ‚‚
        respβ€² = pullr (pb _ _ .pβ‚‚βˆ˜universal) βˆ™ extendl (pb _ _ .square)

    sΞ±β†’ (f , g , h) .left = sym $ pullr (pb _ _ .pβ‚‚βˆ˜universal) βˆ™ assoc _ _ _
    sΞ±β†’ (f , g , h) .right = sym $ pullr (pb _ _ .pβ‚βˆ˜universal) βˆ™ pullr (pb _ _ .pβ‚βˆ˜universal)

  open make-natural-iso
  {-# TERMINATING #-}
  Spanᡇ : Prebicategory _ _ _
  Spanᡇ .Ob = C.Ob
  Spanᡇ .Hom = Spans
  Spanᡇ .id = span _ C.id C.id
  Spanᡇ .compose = Span-∘
  Spanᡇ .unitor-l = to-natural-iso ni where
    ni : make-natural-iso (Id {C = Spans _ _}) _
    ni .eta = sλ←
    ni .inv x .map = pb _ _ .pβ‚‚
    ni .inv x .left = refl
    ni .inv x .right = pb _ _ .square
    ni .eta∘inv x = Span-hom-path (Pullback.uniqueβ‚‚ (pb _ _) {p = idl _ βˆ™ apβ‚‚ C._∘_ refl (introl refl)}
      (pulll (pb _ _ .pβ‚βˆ˜universal))
      (pulll (pb _ _ .pβ‚‚βˆ˜universal))
      (id-comm βˆ™ pb _ _ .square)
      id-comm)
    ni .inv∘eta x = Span-hom-path (pb _ _ .pβ‚‚βˆ˜universal)
    ni .natural x y f = Span-hom-path $
      Pullback.uniqueβ‚‚ (pb _ _) {p = idl _ βˆ™ f .right}
        (pulll (pb _ _ .pβ‚βˆ˜universal) βˆ™ pullr (pb _ _ .pβ‚βˆ˜universal) βˆ™ idl _)
        (pulll (pb _ _ .pβ‚‚βˆ˜universal) βˆ™ pullr (pb _ _ .pβ‚‚βˆ˜universal) βˆ™ idr _)
        (pulll (pb _ _ .pβ‚βˆ˜universal) βˆ™ sym (f .right))
        (pulll (pb _ _ .pβ‚‚βˆ˜universal) βˆ™ idl _)
  Spanᡇ .unitor-r = to-natural-iso ni where
    ni : make-natural-iso (Id {C = Spans _ _}) _
    ni .eta = sρ←
    ni .inv _ .map = pb _ _ .p₁
    ni .inv _ .left = sym (pb _ _ .square)
    ni .inv _ .right = refl
    ni .eta∘inv x = Span-hom-path (Pullback.uniqueβ‚‚ (pb _ _) {p = introl refl}
      (pulll (pb _ _ .pβ‚βˆ˜universal) βˆ™ idl _)
      (pulll (pb _ _ .pβ‚‚βˆ˜universal))
      (idr _)
      (id-comm βˆ™ sym (pb _ _ .square)))
    ni .inv∘eta x = Span-hom-path (pb _ _ .pβ‚βˆ˜universal)
    ni .natural x y f = Span-hom-path $
      Pullback.uniqueβ‚‚ (pb _ _) {p = sym (f .left) βˆ™ introl refl}
        (pulll (pb _ _ .pβ‚βˆ˜universal) βˆ™ pullr (pb _ _ .pβ‚βˆ˜universal) βˆ™ idr _)
        (pulll (pb _ _ .pβ‚‚βˆ˜universal) βˆ™ pullr (pb _ _ .pβ‚‚βˆ˜universal) βˆ™ idl _)
        (pulll (pb _ _ .pβ‚βˆ˜universal) βˆ™ idl _)
        (pulll (pb _ _ .pβ‚‚βˆ˜universal) βˆ™ sym (f .left))
  Spanᡇ .associator = to-natural-iso ni where
    ni : make-natural-iso _ _
    ni .eta = sα←
    ni .inv = sΞ±β†’
    ni .eta∘inv x = Span-hom-path $
      Pullback.uniqueβ‚‚ (pb _ _) {p = pb _ _ .square}
      (pulll (pb _ _ .pβ‚βˆ˜universal) βˆ™ pullr (pb _ _ .pβ‚βˆ˜universal) βˆ™ pb _ _ .pβ‚βˆ˜universal)
      (pulll (pb _ _ .pβ‚‚βˆ˜universal) βˆ™ uniqueβ‚‚ (pb _ _) {p = extendl (pb _ _ .square)}
          (pulll (pb _ _ .pβ‚βˆ˜universal) βˆ™ pullr (pb _ _ .pβ‚βˆ˜universal) βˆ™ pb _ _ .pβ‚‚βˆ˜universal)
          (pulll (pb _ _ .pβ‚‚βˆ˜universal) βˆ™ pb _ _ .pβ‚‚βˆ˜universal)
          refl refl)
      (idr _)
      (idr _)
    ni .inv∘eta x = Span-hom-path $
      Pullback.uniqueβ‚‚ (pb _ _) {p = pb _ _ .square}
      (pulll (pb _ _ .pβ‚βˆ˜universal) βˆ™ uniqueβ‚‚ (pb _ _) {p = extendl (pb _ _ .square)}
        (pulll (pb _ _ .pβ‚βˆ˜universal) βˆ™ pb _ _ .pβ‚βˆ˜universal)
        (pulll (pb _ _ .pβ‚‚βˆ˜universal) βˆ™ pullr (pb _ _ .pβ‚‚βˆ˜universal) βˆ™ pb _ _ .pβ‚βˆ˜universal)
        refl refl)
      (pulll (pb _ _ .pβ‚‚βˆ˜universal) βˆ™ pullr (pb _ _ .pβ‚‚βˆ˜universal) βˆ™ pb _ _ .pβ‚‚βˆ˜universal)
      (idr _)
      (idr _)
    ni .natural x y f = Span-hom-path $ Pullback.uniqueβ‚‚ (pb _ _)
      {p₁' = f .fst .map C.∘ pb _ _ .p₁ C.∘ pb _ _ .p₁}
      {pβ‚‚' = pb _ _ .universal
        {p₁' = f .snd .fst .map C.∘ pb _ _ .pβ‚‚ C.∘ pb _ _ .p₁}
        {pβ‚‚' = f .snd .snd .map C.∘ pb _ _ .pβ‚‚}
        (pulll (sym (f .snd .fst .left)) βˆ™ assoc _ _ _ βˆ™ pb _ _ .square βˆ™ pushl (f .snd .snd .right))}
      {p = sym $ pullr (pb _ _ .pβ‚βˆ˜universal) βˆ™ pulll (sym (f .snd .fst .right)) βˆ™ extendl (sym (pb _ _ .square)) βˆ™ pushl (f .fst .left)}
      (pulll (pb _ _ .pβ‚βˆ˜universal) βˆ™ pullr (pb _ _ .pβ‚βˆ˜universal))
      (pulll (pb _ _ .pβ‚‚βˆ˜universal) βˆ™ pb _ _ .unique
        (pulll (extendl (pb _ _ .pβ‚βˆ˜universal)) βˆ™ pullr (pullr (pb _ _ .pβ‚‚βˆ˜universal)) βˆ™ apβ‚‚ C._∘_ refl (pb _ _ .pβ‚βˆ˜universal))
        (pulll (extendl (pb _ _ .pβ‚‚βˆ˜universal)) βˆ™ pullr (pullr (pb _ _ .pβ‚‚βˆ˜universal)) βˆ™ apβ‚‚ C._∘_ refl (pb _ _ .pβ‚‚βˆ˜universal)))
      (pulll (pb _ _ .pβ‚βˆ˜universal) βˆ™ pullr (pb _ _ .pβ‚βˆ˜universal) βˆ™ pulll (pb _ _ .pβ‚βˆ˜universal) βˆ™ sym (assoc _ _ _))
      (pulll (pb _ _ .pβ‚‚βˆ˜universal) βˆ™ pb _ _ .unique
        (pulll (pb _ _ .pβ‚βˆ˜universal) βˆ™ pullr (pb _ _ .pβ‚βˆ˜universal) βˆ™ extendl (pb _ _ .pβ‚‚βˆ˜universal))
        (pulll (pb _ _ .pβ‚‚βˆ˜universal) βˆ™ pb _ _ .pβ‚‚βˆ˜universal))
  Spanᡇ .triangle f g = Span-hom-path $
    pb _ _ .unique
      (pulll (pb _ _ .pβ‚βˆ˜universal) βˆ™ pullr (pb _ _ .pβ‚βˆ˜universal) βˆ™ pb _ _ .pβ‚βˆ˜universal βˆ™ introl refl)
      (pulll (pb _ _ .pβ‚‚βˆ˜universal) βˆ™ pullr (pb _ _ .pβ‚‚βˆ˜universal) βˆ™ eliml refl)
  Spanᡇ .pentagon f g h i = Span-hom-path $
    Pullback.uniqueβ‚‚ (pb _ _)
      {p = pullr (pulll (pb _ _ .pβ‚‚βˆ˜universal) βˆ™ pullr (pulll (pb _ _ .pβ‚‚βˆ˜universal) βˆ™ pullr (pb _ _ .pβ‚‚βˆ˜universal)) βˆ™ apβ‚‚ C._∘_ refl (pulll (pb _ _ .pβ‚βˆ˜universal)))
         βˆ™ apβ‚‚ C._∘_ refl (extendl (pb _ _ .pβ‚‚βˆ˜universal)) βˆ™ sym (apβ‚‚ C._∘_ refl (idl _ βˆ™ extendl (pb _ _ .pβ‚‚βˆ˜universal)) βˆ™ extendl (sym (pb _ _ .square)))}
      (pulll (pb _ _ .pβ‚βˆ˜universal) βˆ™ pullr (pulll (pb _ _ .pβ‚βˆ˜universal)))
      (pulll (pb _ _ .pβ‚‚βˆ˜universal) βˆ™ pullr (pulll (pb _ _ .pβ‚‚βˆ˜universal) βˆ™ pullr (pb _ _ .pβ‚‚βˆ˜universal)))
      (pulll (pb _ _ .pβ‚βˆ˜universal)
      βˆ™ Pullback.uniqueβ‚‚ (pb _ _) {p = pullr (pb _ _ .pβ‚‚βˆ˜universal) βˆ™ extendl (pb _ _ .square) βˆ™ sym (assoc _ _ _)}
          (pulll (pb _ _ .pβ‚βˆ˜universal) βˆ™ pb _ _ .pβ‚βˆ˜universal)
          (pulll (pb _ _ .pβ‚‚βˆ˜universal) βˆ™ pullr (pb _ _ .pβ‚‚βˆ˜universal))
          (pulll (pb _ _ .pβ‚βˆ˜universal) βˆ™ pb _ _ .unique
            (pulll (pb _ _ .pβ‚βˆ˜universal) βˆ™ pulll (pb _ _ .pβ‚βˆ˜universal) βˆ™ pb _ _ .pβ‚βˆ˜universal βˆ™ idl _)
            (pulll (pb _ _ .pβ‚‚βˆ˜universal) βˆ™ pulll (pullr (pb _ _ .pβ‚‚βˆ˜universal)) βˆ™ pullr (pullr (pb _ _ .pβ‚‚βˆ˜universal) βˆ™ pulll (pb _ _ .pβ‚βˆ˜universal)) βˆ™ pulll (pb _ _ .pβ‚βˆ˜universal)))
          (pulll (pb _ _ .pβ‚‚βˆ˜universal) βˆ™ pullr (pulll (pb _ _ .pβ‚‚βˆ˜universal) βˆ™ pullr (pb _ _ .pβ‚‚βˆ˜universal))
          βˆ™ apβ‚‚ C._∘_ refl (pulll (pb _ _ .pβ‚βˆ˜universal)) βˆ™ pulll (pb _ _ .pβ‚‚βˆ˜universal) βˆ™ sym (assoc _ _ _)))
      ( pulll (pb _ _ .pβ‚‚βˆ˜universal)
      Β·Β· pullr (pb _ _ .pβ‚‚βˆ˜universal)
      Β·Β· sym (idl _ Β·Β· pulll (pb _ _ .pβ‚‚βˆ˜universal) Β·Β· sym (assoc _ _ _)))