module Cat.Bi.Instances.Spans {o β} (C : Precategory o β) where
The bicategory of spansπ
Let be a precategory. By a span in (from an object to an object ), we mean a diagram of the form . Note that the βvertexβ of this span, the object , is part of the data, so that the collection of βspans in β will not be a set (unless is strict) β so we can not construct a category where is the collection of spans from to .
However, we can make spans in the objects of a category, and the hom-sets are the maps in 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
open Span-hom private unquoteDecl eqv = declare-record-iso eqv (quote Span-hom) Span-hom-path : {a b : Ob} {x y : Span a b} {f g : Span-hom x y} β f .map β‘ g .map β f β‘ g Span-hom-path p i .map = p i Span-hom-path {x = x} {y} {f} {g} p i .left j = is-setβsquarep (Ξ» i j β Hom-set _ _) (Ξ» _ β x .left) (Ξ» j β f .left j) (Ξ» j β g .left j) (Ξ» j β y .left β p j) i j Span-hom-path {x = x} {y} {f} {g} p i .right j = is-setβsquarep (Ξ» i j β Hom-set _ _) (Ξ» _ β x .right) (Ξ» j β f .right j) (Ξ» j β g .right j) (Ξ» j β y .right β p j) i j
The category of spans between and admits a faithful functor to (projecting the vertex and the βmiddle mapβ, respectively), so that equality of maps of spans can be compared at the level of maps in .
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 admits pullbacks for arbitrary pairs of maps. Supposing that we have some spans and , we can fit them in an M-shaped diagram like
so that taking the pullback of the diagram
gives us an universal solution to the problem of finding a span
.
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
),
.
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
is univalent, then
is locally so, and when
is gaunt, then
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 is implemented by a pullback diagram like
but observe that the maps and also form a cone over the cospan , 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 . 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 _ _ _)))