{-# OPTIONS --lossy-unification -vtc.def.fun:10 #-} open import Cat.Instances.Sets.Complete open import Cat.Bi.Instances.Spans open import Cat.Bi.Diagram.Monad open import Cat.Instances.Sets open import Cat.Bi.Base open import Cat.Prelude 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) 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 . 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 _ _ 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 .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 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 (Ξ» _ β 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) _ _))))