module Cat.Bi.Instances.Spans {o ℓ} (C : Precategory o ℓ) where

The bicategory of spans🔗

Let $C$ be a precategory. By a span in $C$ (from an object $A : C$ to an object $B : C),$ we mean a diagram of the form $A \leftarrow C \to B .$ Note that the “vertex” of this span, the object $C,$ is part of the data, so that the collection of “spans in $C$ ” will not be a set (unless $C$ is strict) — so we can not construct a category where $Hom (a, b)$ is the collection of spans from $a$ to $b .$

However, we can make spans in $C$ the objects of a category, and the hom-sets are the maps in $C$ between the vertices which “commute with the legs”. Diagrammatically, 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)$ of spans between $A$ and $B$ admits a faithful functor to $C$ (proecting the vertex and the “middle map”, respectively), so that equality of maps of spans can be compared at the level of maps in $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 _ _ = 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$ admits pullbacks for arbitrary pairs of maps. Supposing that we have some spans $S : A \to B$ and $S^{'} : B \to C,$ we can fit them in an M-shaped diagram like

so that taking the pullback of the diagram $S \to B \leftarrow S^{'}$ gives us an universal solution to the problem of finding a span $A \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 _ (pullbacks : Pullbacks C) where
  open Pullbacks pullbacks
  open Functor

  Span-∘ : ∀ {a b c} → Functor (Spans b c ×ᶜ Spans a b) (Spans a c)
  Span-∘ .F₀ (sp1 , sp2) =
    span (Pb (sp1 .left) (sp2 .right)) (sp2 .left ∘ p₂ _ _) (sp1 .right ∘ p₁ _ _)

  Span-∘ .F₁ {x1 , x2} {y1 , y2} (f , g) = res
    where
      x→y : Hom (Pb (x1 .left) (x2 .right)) (Pb (y1 .left) (y2 .right))
      x→y = pb (f .map ∘ p₁ _ _) (g .map ∘ p₂ _ _) comm
        where abstract
          comm : y1 .left ∘ f .map ∘ p₁ (x1 .left) (x2 .right) ≡ y2 .right ∘ g .map ∘ p₂ _ _
          comm = pulll (sym (f .left)) ∙ square ∙ pushl (g .right)

      res : Span-hom _ _
      res .map = x→y
      res .left = sym (pullr p₂∘pb ∙ pulll (sym (g .left)))
      res .right = sym (pullr p₁∘pb ∙ pulll (sym (f .right)))

  Span-∘ .F-id {x1 , x2} = Span-hom-path $ sym $ pb-unique id-comm id-comm

  Span-∘ .F-∘ {x1 , x2} {y1 , y2} {z1 , z2} f g =
    Span-hom-path $ sym $ pb-unique
      (pulll p₁∘pb ∙ pullr p₁∘pb ∙ assoc _ _ _)
      (pulll p₂∘pb ∙ pullr p₂∘pb ∙ assoc _ _ _)

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),$ $Spans (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$ is univalent, then $Spans (C)$ is locally so, and when $C$ is gaunt, then $Spans (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 \circ S$ is implemented by a pullback diagram like

but observe that the maps $S f A$ and $S id S$ also form a cone over the cospan $A \to A 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 \circ S \Rightarrow S .$ The right unitor is analogous.

  open Prebicategory

  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 _ _ id-comm-sym
    sλ← x .left  = sym $ pullr p₂∘pb ∙ idr _
    sλ← x .right = sym $ pullr p₁∘pb ∙ idl _

    sρ← : ∀ {A B} (x : Span A B) → Span-hom x (x ¤ span _ C.id C.id)
    sρ← x .map   = pb _ _ id-comm
    sρ← x .left  = sym $ pullr p₂∘pb ∙ idl _
    sρ← x .right = sym $ pullr p₁∘pb ∙ idr _

For the associator, while doing the construction in elementary terms is quite complicated, we observe that, diagrammatically, 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 _ _ resp' where
      abstract
        resp : g .left C.∘ p₂ (f .left) (g .right)
           C.∘ p₁ ((f ¤ g) .left) (h .right)
             ≡ h .right C.∘ p₂ ((f ¤ g) .left) (h .right)
        resp = assoc _ _ _ ∙ square

      shuffle = pb (p₂ _ _ C.∘ p₁ _ _) (p₂ _ _) resp

      abstract
        resp' : f .left C.∘ p₁ (f .left) (g .right)
            C.∘ p₁ ((f ¤ g) .left) (h .right)
              ≡ (g ¤ h) .right C.∘ shuffle
        resp' = sym $ pullr p₁∘pb ∙ extendl (sym (square))

    sα← (f , g , h) .left = sym $ pullr p₂∘pb ∙ pullr p₂∘pb
    sα← (f , g , h) .right = sym $ pullr p₁∘pb ∙ 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 _ _ resp' where
      abstract
        resp : f .left C.∘ p₁ (f .left) ((g ¤ h) .right)
             ≡ g .right C.∘ p₁ (g .left) (h .right)
           C.∘ p₂ (f .left) ((g ¤ h) .right)
        resp = square ∙ sym (assoc _ _ _)

      shuffle = pb (p₁ _ _) (p₁ _ _ C.∘ p₂ _ _) resp

      abstract
        resp' : (f ¤ g) .left C.∘ shuffle
              ≡ h .right C.∘ p₂ (g .left) (h .right)
            C.∘ p₂ (f .left) ((g ¤ h) .right)
        resp' = pullr p₂∘pb ∙ extendl square

    sα→ (f , g , h) .left = sym $ pullr p₂∘pb ∙ assoc _ _ _
    sα→ (f , g , h) .right = sym $ pullr p₁∘pb ∙ pullr p₁∘pb

  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 = p₂ _ _
    ni .inv x .left = refl
    ni .inv x .right = square
    ni .eta∘inv x = Span-hom-path (pb-unique₂ {p = idl _ ∙ ap₂ C._∘_ refl (introl refl)}
      (pulll p₁∘pb)
      (pulll p₂∘pb)
      (id-comm ∙ square)
      id-comm)
    ni .inv∘eta x = Span-hom-path p₂∘pb
    ni .natural x y f = Span-hom-path $
      pb-unique₂ {p = idl _ ∙ f .right}
        (pulll p₁∘pb ∙ pullr p₁∘pb ∙ idl _)
        (pulll p₂∘pb ∙ pullr p₂∘pb ∙ idr _)
        (pulll p₁∘pb ∙ sym (f .right))
        (pulll p₂∘pb ∙ idl _)
  Spanᵇ .unitor-r = to-natural-iso ni where
    ni : make-natural-iso (Id {C = Spans _ _}) _
    ni .eta = sρ←
    ni .inv _ .map = p₁ _ _
    ni .inv _ .left = sym (square)
    ni .inv _ .right = refl
    ni .eta∘inv x = Span-hom-path (pb-unique₂ {p = introl refl}
      (pulll p₁∘pb ∙ idl _)
      (pulll p₂∘pb)
      (idr _)
      (id-comm ∙ sym (square)))
    ni .inv∘eta x = Span-hom-path p₁∘pb
    ni .natural x y f = Span-hom-path $
      pb-unique₂ {p = sym (f .left) ∙ introl refl}
        (pulll p₁∘pb ∙ pullr p₁∘pb ∙ idr _)
        (pulll p₂∘pb ∙ pullr p₂∘pb ∙ idl _)
        (pulll p₁∘pb ∙ idl _)
        (pulll p₂∘pb ∙ 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 $
      pb-unique₂ {p = square}
      (pulll p₁∘pb ∙ pullr p₁∘pb ∙ p₁∘pb)
      (pulll p₂∘pb ∙ pb-unique₂ {p = extendl (square)}
          (pulll p₁∘pb ∙ pullr p₁∘pb ∙ p₂∘pb)
          (pulll p₂∘pb ∙ p₂∘pb)
          refl refl)
      (idr _)
      (idr _)
    ni .inv∘eta x = Span-hom-path $
      pb-unique₂ {p = square}
      (pulll p₁∘pb ∙ pb-unique₂ {p = extendl (square)}
        (pulll p₁∘pb ∙ p₁∘pb)
        (pulll p₂∘pb ∙ pullr p₂∘pb ∙ p₁∘pb)
        refl refl)
      (pulll p₂∘pb ∙ pullr p₂∘pb ∙ p₂∘pb)
      (idr _)
      (idr _)
    ni .natural x y f = Span-hom-path $ pb-unique₂
      {p₁' = f .fst .map C.∘ p₁ _ _ C.∘ p₁ _ _}
      {p₂' = pb
          (f .snd .fst .map C.∘ p₂ _ _ C.∘ p₁ _ _)
          (f .snd .snd .map C.∘ p₂ _ _)
          (pulll (sym (f .snd .fst .left)) ∙ assoc _ _ _ ∙ square ∙ pushl (f .snd .snd .right))}
      {p = sym $ pullr p₁∘pb ∙ pulll (sym (f .snd .fst .right)) ∙ extendl (sym (square)) ∙ pushl (f .fst .left)}
      (pulll p₁∘pb ∙ pullr p₁∘pb)
      (pulll p₂∘pb ∙ pb-unique
        (pulll (extendl p₁∘pb) ∙ pullr (pullr p₂∘pb) ∙ ap₂ C._∘_ refl p₁∘pb)
        (pulll (extendl p₂∘pb) ∙ pullr (pullr p₂∘pb) ∙ ap₂ C._∘_ refl p₂∘pb))
      (pulll p₁∘pb ∙ pullr p₁∘pb ∙ pulll p₁∘pb ∙ sym (assoc _ _ _))
      (pulll p₂∘pb ∙ pb-unique
        (pulll p₁∘pb ∙ pullr p₁∘pb ∙ extendl p₂∘pb)
        (pulll p₂∘pb ∙ p₂∘pb))
  Spanᵇ .triangle f g = Span-hom-path $
    pb-unique
      (pulll p₁∘pb ∙ pullr p₁∘pb ∙ p₁∘pb ∙ introl refl)
      (pulll p₂∘pb ∙ pullr p₂∘pb ∙ eliml refl)
  Spanᵇ .pentagon f g h i = Span-hom-path $
    pb-unique₂
      {p = pullr (pulll p₂∘pb ∙ pullr (pulll p₂∘pb ∙ pullr p₂∘pb) ∙ ap₂ C._∘_ refl (pulll p₁∘pb))
         ∙ ap₂ C._∘_ refl (extendl p₂∘pb) ∙ sym (ap₂ C._∘_ refl (idl _ ∙ extendl p₂∘pb) ∙ extendl (sym (square)))}
      (pulll p₁∘pb ∙ pullr (pulll p₁∘pb))
      (pulll p₂∘pb ∙ pullr (pulll p₂∘pb ∙ pullr p₂∘pb))
      (pulll p₁∘pb
      ∙ pb-unique₂ {p = pullr p₂∘pb ∙ extendl (square) ∙ sym (assoc _ _ _)}
          (pulll p₁∘pb ∙ p₁∘pb)
          (pulll p₂∘pb ∙ pullr p₂∘pb)
          (pulll p₁∘pb ∙ pb-unique
            (pulll p₁∘pb ∙ pulll p₁∘pb ∙ p₁∘pb ∙ idl _)
            (pulll p₂∘pb ∙ pulll (pullr p₂∘pb) ∙ pullr (pullr p₂∘pb ∙ pulll p₁∘pb) ∙ pulll p₁∘pb))
          (pulll p₂∘pb ∙ pullr (pulll p₂∘pb ∙ pullr p₂∘pb)
          ∙ ap₂ C._∘_ refl (pulll p₁∘pb) ∙ pulll p₂∘pb ∙ sym (assoc _ _ _)))
      ( pulll p₂∘pb
      ·· pullr p₂∘pb
      ·· sym (idl _ ·· pulll p₂∘pb ·· sym (assoc _ _ _)))