module Cat.Monoidal.Instances.Day {β} {C : Precategory β β} (cmon : Monoidal-category C) where
The Day convolution productπ
The Day convolution monoidal structure on is the free cocompletion of a small monoidal category within the context of monoidal categories: its monoidal cocompletion. This uniquely determines the construction of which is perhaps sufficient motivation to a category theorist. However, itβs worth pointing out that the Day convolution comes up in practice surprisingly often, so that the motivation for this page does not rest entirely on abstract nonsense. Here are a few examples, before we get started:
Automata theory: If we have a set which we call the alphabet, then, as usual, we call a subset a language on Languages are closed under the generic operations of intersection and union of subsets, but we also have an operation specific to this domain: concatenation, which arises from the free monoid structure on
More concretely, the concatenation is the subset which, expressed as a predicate, has value
That is, the words belonging to are precisely those which decompose as a concatenation of a word from followed by a word from The operation of concatenation preserves joins in each variable: We can calculate
and the other variable is symmetric. To give a concrete example, we can define the Kleene star where denotes the composition. Then our cocontinuity result says that we can compute concatenation with a star as a union of simpler concatenations. For example, an enumeration of starts
Algebra: if we have a group and a ring there is a universal way to equip the free module with a multiplication that makes it into a ring, and where this multiplication is also in each variable: the group , which we also refer to as For simplicity, let us assume that is a finite group.
Note that, since is finite, we can take the elements of to simply be arbitrary functions If we think of as a polynomial, then we associate to it the function that sends each to the element which appears as its coefficient. In the other direction, an assignment of coefficients determines the polynomial
The multiplication on is determined uniquely by the requirement that it extends the multiplication on in an way: for polynomials we should have
It is not immediately obvious that we can rewrite this double summation in βcoefficient formβ. But if we recall the diagonal function defined so that if (and otherwise), then we can express this as
since, intuitively, we have = since, for each value of if we do not have then the summand is equal to zero.
Drawing a generalisation from the cases above, we can equip the collection of functions with a monoid structure whenever and are monoids, and admits an operation for aggregation over , to play the role of the existential quantifier and summation. Writing for this aggregation operation, the product is given pointwise by
This operation is generally referred to as the convolution product of and and it can be seen as the special case of the Day convolution where the domain is a discrete category.
For those curious but unfamiliar with the abstract nonsense, we should explain what, exactly, is meant by monoidal cocompletion: in addition to showing that is cocomplete, and equipping it with a monoidal structure we must show that these behave nicely together:
The tensor product we construct must be cocontinuous in each variable;
Our chosen cocompletion which in this case is the Yoneda embedding must be a strong monoidal functor: We should have 1
As usual when we have an object defined by a universal property, the Day convolution monoidal structure is unique: making this particular case explicit, given any other monoidal cocompletion we have a unique equivalence of monoidal categories Among the univalent monoidal categories, we may sharpen this result to saying that has a contractible space of monoidal cocompletions.
The constructionπ
We will interpret the formula above literally, relying on the fact that coends are also written with an integral sign. To generalise away from a discrete domain, we must express the idea of decomposing an object into parts without the use of equality. An obvious idea would be isomorphism, but this turns out to be too strong: we can simply take the product with the into the product:
Itβs worth taking a second to read the formalised definition, below, if you are unfamiliar with coends. We must express the βintegrandβ as a functor This provides us with βpolarisedβ versions of the variables which we write and
We then distribute these variables according to the polarities of each functor. Since is covariant in its second argument, it sees but the presheaves are contravariant, so we have factors and
module Day (X Y : β PSh β C β) where Day-diagram : Ob β Functor ((C ΓαΆ C) ^op ΓαΆ (C ΓαΆ C)) (Sets β) β£ Day-diagram c .Fβ ((cββ» , cββ») , cββΊ , cββΊ) β£ = Hom c (cββΊ β cββΊ) Γ (X Κ» cββ») Γ (Y Κ» cββ»)
Day-diagram c .Fβ ((cββ» , cββ») , cββΊ , cββΊ) .is-tr = Γ-is-hlevel 2 (Hom-set _ _) (Γ-is-hlevel 2 (X .Fβ _ .is-tr) (Y .Fβ _ .is-tr)) Day-diagram c .Fβ ((fβ» , gβ») , fβΊ , gβΊ) (h , x , y) = (fβΊ ββ gβΊ) β h , X .Fβ fβ» x , Y .Fβ gβ» y Day-diagram c .F-id = ext Ξ» h x y β eliml (-β- .F-id) , X .F-id #β x , Y .F-id #β y Day-diagram c .F-β f g = ext Ξ» h x y β pushl (-β- .F-β _ _) , X .F-β _ _ #β _ , Y .F-β _ _ #β _
opaque Day-coend : (c : Ob) β Coend (Day-diagram c) Day-coend c = Set-coend (Day-diagram c)
We shall now repeat some of our knowledge about coends valued in sets, but specialised to the case of the Day convolution. First, we note that we can write the elements of the coend (at as triples where and
day : {i a b : Ob} (h : Hom i (a β b)) (x : X Κ» a) (y : Y Κ» b) β Day.nadir Κ» i day h x y = inc ((_ , _) , h , x , y)
day-ap : {i a b : Ob} {h h' : Hom i (a β b)} {x x' : X Κ» a} {y y' : Y Κ» b} β h β‘ h' β x β‘ x' β y β‘ y' β day h x y β‘ day h' x' y' day-ap {a = a} {b} p q r i = inc ((a , b) , p i , q i , r i) day-apβ : β {i a b} {h h' : Hom i (a β b)} {x y} β h β‘ h' β day h x y β‘ day h' x y day-apβ p = day-ap p refl refl
Moreover, these triples have identifications generated by letting be whenever these both make sense. More generally, we have equal to whenever
day-glue : {i a b a' b' : Ob} {f : Hom a' a} {g : Hom b' b} {h : Hom i (a' β b')} {x : X Κ» a} {y : Y Κ» b} β {fgh : Hom i (a β b)} (p : fgh β‘ (f ββ g) β h) β day fgh x y β‘ day h (X .Fβ f x) (Y .Fβ g y) day-glue {i} {a} {b} {a'} {b'} {f} {g} {h} {x} {y} {fgh} p = day fgh x y β‘β¨ day-ap p (sym (X .F-id) #β x) (sym (Y .F-id) #β y) β©β‘ day ((f ββ g) β h) (X .Fβ id x) (Y .Fβ id y) β‘β¨ Coeq.glue {f = dimapl (Day-diagram i)} {g = dimapr (Day-diagram i)} ((a , b) , (a' , b') , (f , g) , h , x , y) β©β‘ day ((id ββ id) β h) (X .Fβ f x) (Y .Fβ g y) β‘β¨ day-apβ (eliml β.F-id) β©β‘ day h (X .Fβ f x) (Y .Fβ g y) β
Finally, we will use the formalism of cowedges to define functions out of Essentially, this says that we can define a function whenever we can define in a way compatible with the relation above.
factor : β {i} (W : Cowedge (Day-diagram i)) β Day.nadir Κ» i β β W .nadir β factor W = Day.factor _ W
factor-day : β {i a b} {W : Cowedge (Day-diagram i)} {h : Hom i (a β b)} {x : X Κ» a} {y : Y Κ» b} β factor W (day h x y) β‘ W .Ο (a , b) (h , x , y) factor-day = refl {-# REWRITE factor-day #-} -- To have better type inference we define the Day-coend and its -- associated projections as opaque symbols. Agda will treat them as -- injective so e.g. an equation between `Day.nadir F G i = Day.nadir -- ? ? ?` will actually solve those three metas. -- -- But, of course, opaque symbols don't compute, and we'd really -- really like to have `factor W (day h x y) = W .Ο h x y`. One -- approach would be to lift everything that needs this definitional -- equality into an opaque block, but that would massively bloat the -- file with mandatory type signatures. -- -- Rewrite rules to the rescue: `factor-day` allows us to "export" the -- computation rule for `factor W (day ...)` without exposing the -- computational behaviour of any other of the symbols here. private extensional-work : β {i β' βr} {C : Type β'} β¦ _ : H-Level C 2 β¦ β β¦ sf : β {a b} β Extensional ((h : Hom i (a β b)) (x : X Κ» a) (y : Y Κ» b) β C) βr β¦ β Extensional (β Day.nadir i β β C) (β β βr) extensional-work {i} {C = C} β¦ sf β¦ = done where T : Type _ T = {a b : Ob} (h : Hom i (a β b)) (x : X Κ» a) (y : Y Κ» b) β C unday : (β Day.nadir i β β C) β T unday f h x y = f (day h x y) opaque unfolding Day-coend day -- Note: Extensional-day-map and Extensional-coeq-map well and -- truly overlap whenever Day.nadir is unfoldable (which it is -- in the definition of to-p). So we can't let to-p see -- Extensional-day-map as an instance. to-p : β {f g} β Path T (unday f) (unday g) β f β‘ g to-p p = ext Ξ» a b h x y i β p i {a} {b} h x y done : Extensional (β Day.nadir i β β C) _ done = injectionβextensional (hlevel 2) to-p auto instance Extensional-day-map : β {i β' βr} {C : Type β'} β¦ _ : H-Level C 2 β¦ β β¦ sf : β {a b} β Extensional ((h : Hom i (a β b)) (x : X Κ» a) (y : Y Κ» b) β C) βr β¦ β Extensional (β Day.nadir i β β C) (β β βr) Extensional-day-map = extensional-work day-swap : β {i a b a' b'} {f : Hom a' a} {g : Hom b' b} {h : Hom i (a' β b')} {a'' b''} {f' : Hom a'' a} {g' : Hom b'' b} {h' : Hom i (a'' β b'')} {x : X Κ» a} {y : Y Κ» b} β (f ββ g) β h β‘ (f' ββ g') β h' β day h (X .Fβ f x) (Y .Fβ g y) β‘ day h' (X .Fβ f' x) (Y .Fβ g' y) day-swap p = sym (day-glue refl) Β·Β· day-apβ p Β·Β· day-glue refl
As an example of constructing a map using cowedges, we can construct the restriction given Pointwise, this sends to Itβs a straightforward-but-annoying calculation to show that this extends to the quotient.
Day-cowedge : β {x} {y} β Hom y x β Cowedge (Day-diagram x) Day-cowedge {y = y} h .nadir = Day.nadir y Day-cowedge h .Ο (a , b) (f , x , y) = day (f β h) x y Day-cowedge h .extranatural {a , b} {a' , b'} (f , g) = funext Ξ» (i , x , y) β day (((f ββ g) β i) β h) (X .Fβ id x) (Y .Fβ id y) β‘β¨ day-ap refl (X .F-id #β x) (Y .F-id #β y) β©β‘ day (((f ββ g) β i) β h) x y β‘β¨ day-glue (sym (assoc _ _ _)) β©β‘ day (i β h) (X .Fβ f x) (Y .Fβ g y) β‘β¨ day-apβ (introl β.F-id β assoc _ _ _) β©β‘ day (((id ββ id) β i) β h) (X .Fβ f x) (Y .Fβ g y) β _βα΄°_ : β PSh β C β _βα΄°_ .Fβ c = Day.nadir c _βα΄°_ .Fβ {x} {y} h v = factor (Day-cowedge h) v _βα΄°_ .F-id = ext Ξ» h x y β day-apβ (idr h) _βα΄°_ .F-β f g = ext Ξ» h x y β day-apβ (assoc h g f)
infix 25 _βα΄°_ module _ {X Y} where open Day X Y using (day ; day-ap ; day-apβ ; day-swap ; Extensional-day-map ; day-glue) renaming (factor to Day-rec) public open Day using (_βα΄°_ ; Day-diagram)
Together with some quick functoriality proofs, we have shown above that the Day convolution is a presheaf. If we have natural transformations and then we can extend these to a so that we actually have a functor This is but another annoying calculation.
Day-bifunctor-cowedge : β {X Y X' Y' : β PSh β C β} {i} β X => X' β Y => Y' β Cowedge (Day-diagram X Y i) Day-bifunctor-cowedge {X} {Y} {X'} {Y'} {i} F G = go where private module D = Day X' Y' go : Cowedge (Day-diagram X Y i) go .nadir = D.nadir i go .Ο c (h , x , y) = D.day h (F .Ξ· _ x) (G .Ξ· _ y) go .extranatural (f , g) = ext Ξ» h x y β D.day ((f ββ g) β h) (F .Ξ· _ (X .Fβ id x)) (G .Ξ· _ (Y .Fβ id y)) β‘β¨ D.day-ap refl (F .is-natural _ _ id #β _) (G .is-natural _ _ id #β _) β©β‘ D.day ((f ββ g) β h) (X' .Fβ id (F .Ξ· _ x)) (Y' .Fβ id (G .Ξ· _ y)) β‘β¨ D.day-swap (extendl (eliml β.F-id β intror β.F-id)) β©β‘ D.day ((id ββ id) β h) (X' .Fβ f (F .Ξ· _ x)) (Y' .Fβ g (G .Ξ· _ y)) β‘Λβ¨ D.day-ap refl (F .is-natural _ _ f #β _) (G .is-natural _ _ g #β _) β©β‘Λ D.day ((id ββ id) β h) (F .Ξ· _ (X .Fβ f x)) (G .Ξ· _ (Y .Fβ g y)) β Day-map : β {X X' Y Y'} (F : X => X') (G : Y => Y') β X βα΄° Y => X' βα΄° Y' Day-map F G .Ξ· i = Day-rec (Day-bifunctor-cowedge F G) Day-map F G .is-natural x y f = trivial! Day-bifunctor : Functor (PSh β C ΓαΆ PSh β C) (PSh β C) Day-bifunctor .Fβ (X , Y) = X βα΄° Y Day-bifunctor .Fβ (F , G) = Day-map F G Day-bifunctor .F-id = trivial! Day-bifunctor .F-β f g = trivial!
The monoidal structureπ
The rest of this module is devoted to showing that the Day convolution is actually a monoidal structure: that is, we have unitors and an associator, which satisfy the triangle and pentagon identities. We will give an overview of the constructor of the right unitor, Itβs a representative example of the nasty calculations to come.
Fixing a presheaf and coordinate we want to show that
is isomorphic to Were we not working in a proof assistant, we could do this by coend calculus: itβs an instance of the Yoneda lemma. However, it will be much easier in the long run to bang out an explicit isomorphism. At the level of points, we are given and We must produce an element of The composite
acts on to give us precisely the element we want. In the other direction, we can send to We can then perform the extremely annoying calculations to show that (a) this map extends to the coend, (b) the resulting map is a natural transformation, and (c) the inverse construction we sketched is actually an inverse.
module _ (X : β PSh β C β) where idr-to-cowedge : β x β Cowedge (Day-diagram X (γβ C Unit) x) idr-to-cowedge i .nadir = X # i idr-to-cowedge i .Ο (a , b) (h , x , y) = X .Fβ (Οβ β (id ββ y) β h) x idr-to-cowedge i .extranatural {a , b} {a' , b'} (f , g) = ext Ξ» h x y β X .Fβ (Οβ β (id ββ y β id) β (f ββ g) β h) (X .Fβ id x) β‘β¨ apβ (X .Fβ) (ap (Οβ β_) (β.pulll (apβ _,_ (idl f) (ap (_β g) (idr y))))) refl β©β‘ X .Fβ (Οβ β (f ββ y β g) β h) (X .Fβ id x) β‘β¨ apβ (X .Fβ) (ap (Οβ β_) (β.pushl (apβ _,_ (intror refl) (introl refl)))) refl β©β‘ X .Fβ (Οβ β (f ββ id) β (id ββ y β g) β h) (X .Fβ id x) β‘β¨ apβ (X .Fβ) (extendl (unitor-r .IsoβΏ.from .is-natural a a' f)) refl β©β‘ X .Fβ (f β Οβ β (id ββ y β g) β h) (X .Fβ id x) β‘β¨ X .F-β _ _ #β _ β©β‘ X .Fβ (Οβ β (id ββ y β g) β h) (X .Fβ f (X .Fβ id x)) β‘β¨ apβ (X .Fβ) (ap (Οβ β_) (apβ _β_ refl (introl β.F-id))) (ap (X .Fβ f) (X .F-id #β x)) β©β‘ X .Fβ (Οβ β (id ββ y β g) β (id ββ id) β h) (X .Fβ f x) β Day-idr : X βα΄° γβ C Unit β βΏ X Day-idr = to-natural-iso mk-idr where mk-idr : make-natural-iso (X βα΄° γβ C Unit) X mk-idr .eta x = Day-rec (idr-to-cowedge x) mk-idr .inv x a = day Οβ a id mk-idr .etaβinv x = ext Ξ» a β apβ (X .Fβ) (ap (Οβ β_) (eliml β.F-id) β unitor-r .IsoβΏ.invr Ξ·β _) refl β (X .F-id #β a) mk-idr .invβeta i = ext Ξ» h x y β day Οβ (X .Fβ (Οβ β (id ββ y) β h) x) id β‘β¨ day-ap refl refl (introl refl) β©β‘ day Οβ (X .Fβ (Οβ β (id ββ y) β h) x) (id β id) β‘β¨ day-swap (sym (unitor-r .IsoβΏ.to .is-natural _ _ _) β cancell (unitor-r .IsoβΏ.invl Ξ·β _)) β©β‘ day h (X .Fβ id x) (id β y) β‘β¨ day-ap refl (X .F-id #β x) (idl y) β©β‘ day h x y β mk-idr .natural x y f = ext Ξ» h x y β X .Fβ f (X .Fβ (Οβ β (id ββ y) β h) x) β‘β¨ sym (X .F-β _ _) #β _ β©β‘ X .Fβ ((Οβ β (id ββ y) β h) β f) x β‘β¨ apβ (X .Fβ) (pullr (pullr refl)) refl β©β‘ X .Fβ (Οβ β (id ββ y) β h β f) x β
This completes the construction of the right unitor. It also completes the commentary on this module: the construction of the left unitor, is analogous: just flip everything. The construction of the associator must be done in steps. However, at the level of points, these are all trivial operations, and the vast majority of this module is dedicated to (extra)naturality conditions and proofs of isomorphy.
module _ (Y : β PSh β C β) where idl-to-cowedge : β x β Cowedge (Day-diagram (γβ C Unit) Y x) idl-to-cowedge i .nadir = Y # i idl-to-cowedge i .Ο (a , b) (h , x , y) = Y .Fβ (Ξ»β β (x ββ id) β h) y idl-to-cowedge i .extranatural {a , b} {a' , b'} (f , g) = ext Ξ» h x y β apβ (Y .Fβ) (ap (Ξ»β β_) (β.extendl (apβ _,_ (ap (_β f) (idr x) β introl refl) id-comm-sym)) β extendl (unitor-l .IsoβΏ.from .is-natural _ _ _)) (Y .F-id #β y) Β·Β· (Y .F-β _ _ #β y) Β·Β· apβ (Y .Fβ) (ap (Ξ»β β_) (apβ _β_ refl (introl β.F-id))) refl Day-idl : γβ C Unit βα΄° Y β βΏ Y Day-idl = to-natural-iso mk-idl where mk-idl : make-natural-iso (γβ C Unit βα΄° Y) Y mk-idl .eta x = Day-rec (idl-to-cowedge x) mk-idl .inv x a = day Ξ»β id a mk-idl .etaβinv x = ext Ξ» a β apβ (Y .Fβ) (ap (Ξ»β β_) (eliml β.F-id) β unitor-l .IsoβΏ.invr Ξ·β _) refl β (Y .F-id #β a) mk-idl .invβeta i = ext Ξ» h x y β day Ξ»β id (Y .Fβ (Ξ»β β (x ββ id) β h) y) β‘β¨ day-ap refl (introl refl) refl β©β‘ day Ξ»β (id β id) (Y .Fβ (Ξ»β β (x ββ id) β h) y) β‘β¨ day-swap (sym (unitor-l .IsoβΏ.to .is-natural _ _ _) β cancell (unitor-l .IsoβΏ.invl Ξ·β _)) β©β‘ day h (id β x) (Y .Fβ id y) β‘β¨ day-ap refl (idl x) (Y .F-id #β y) β©β‘ day h x y β mk-idl .natural = Ξ» x y f β ext Ξ» h x y β Y .Fβ f (Y .Fβ (Ξ»β β (x ββ id) β h) y) β‘Λβ¨ Y .F-β _ _ #β _ β©β‘Λ Y .Fβ ((Ξ»β β (x ββ id) β h) β f) y β‘β¨ apβ (Y .Fβ) (pullr (pullr refl)) refl β©β‘ Y .Fβ (Ξ»β β (x ββ id) β h β f) y β module _ (X Y Z : β PSh β C β) where assoc-toβ : β i {a b} (h : Hom i (a β b)) (z : Z Κ» b) β Cowedge (Day-diagram X Y a) assoc-toβ i h z .nadir = Day.nadir X (Y βα΄° Z) i assoc-toβ i h z .Ο (a' , b') (h' , x , y) = day (Ξ±β _ _ _ β (h' ββ id) β h) x (day id y z) assoc-toβ i h z .extranatural (f , g) = ext Ξ» h' x y β day (Ξ±β _ _ _ β ((f ββ g) β h' ββ id) β h) (X .Fβ id x) (day id (Y .Fβ id y) z) β‘β¨ day-ap (ap (Ξ±β _ _ _ β_) (β.pushl (apβ _,_ refl (introl refl)))) (X .F-id #β x) (day-ap refl (Y .F-id #β y) refl) β©β‘ day (Ξ±β _ _ _ β ((f ββ g) ββ id) β (h' ββ id) β h) x (day id y z) β‘β¨ day-apβ (extendl (associator .IsoβΏ.to .is-natural _ _ _)) β©β‘ day ((f ββ (g ββ id)) β Ξ±β _ _ _ β (h' ββ id) β h) x (day id y z) β‘β¨ day-glue refl β©β‘ day (Ξ±β _ _ _ β (h' ββ id) β h) (X .Fβ f x) (day (id β (g ββ id)) y z) β‘β¨ day-ap (ap (Ξ±β _ _ _ β_) (ap (_β h) (apβ _ββ_ (introl β.F-id) refl))) refl (day-apβ id-comm-sym Β·Β· day-glue refl Β·Β· day-ap refl refl (Z .F-id #β z)) β©β‘ day (Ξ±β _ _ _ β ((id ββ id) β h' ββ id) β h) (X .Fβ f x) (day id (Y .Fβ g y) z) β assoc-to-cowedge : β i β Cowedge (Day-diagram (X βα΄° Y) Z i) assoc-to-cowedge i .nadir = Day.nadir X (Y βα΄° Z) i assoc-to-cowedge i .Ο (a , b) (h , x , y) = Day-rec (assoc-toβ i h y) x assoc-to-cowedge i .extranatural (f , g) = ext Ξ» h h' x y z β day (Ξ±β _ _ _ β (h' β id ββ id) β (f ββ g) β h) x (day id y (Z .Fβ id z)) β‘β¨ day-ap (ap (Ξ±β _ _ _ β_) (β.extendl (apβ _,_ (ap (_β f) (idr h') β introl β.F-id) id-comm-sym))) refl (day-ap refl refl (Z .F-id #β z)) β©β‘ day (Ξ±β _ _ _ β ((id ββ id) ββ g) β (h' β f ββ id) β h) x (day id y z) β‘β¨ day-apβ (extendl (associator .IsoβΏ.to .is-natural _ _ _)) β©β‘ day ((id ββ (id ββ g)) β Ξ±β _ _ _ β (h' β f ββ id) β h) x (day id y z) β‘β¨ day-glue refl β©β‘ day (Ξ±β _ _ _ β (h' β f ββ id) β h) (X .Fβ id x) (day (id β (id ββ g)) y z) β‘β¨ day-ap (ap (Ξ±β _ _ _ β_) (apβ _β_ refl (introl β.F-id))) (X .F-id #β x) (day-glue id-comm-sym β day-ap refl (Y .F-id #β y) refl) β©β‘ day (Ξ±β _ _ _ β (h' β f ββ id) β (id ββ id) β h) x (day id y (Z .Fβ g z)) β assoc-fromβ : β i {a b} (h : Hom i (a β b)) (x : X Κ» a) β Cowedge (Day-diagram Y Z b) assoc-fromβ i h x .nadir = Day.nadir (X βα΄° Y) Z i assoc-fromβ i h x .Ο (a' , b') (h' , y , z) = day (Ξ±β _ _ _ β (id ββ h') β h) (day id x y) z assoc-fromβ i h x .extranatural (f , g) = ext Ξ» h' y z β day (Ξ±β _ _ _ β (id ββ ((f ββ g) β h')) β h) (day id x (Y .Fβ id y)) (Z .Fβ id z) β‘β¨ day-ap (extendl (pushr (apβ _ββ_ (introl refl) refl β β.F-β _ _) Β·Β· pullr refl Β·Β· extendl (associator .IsoβΏ.from .is-natural _ _ _))) (day-ap refl refl (Y .F-id #β y)) (Z .F-id #β z) β©β‘ day (((id ββ f) ββ g) β (Ξ±β _ _ _ β (id ββ h')) β h) (day id x y) z β‘β¨ day-glue refl β©β‘ day ((Ξ±β _ _ _ β (id ββ h')) β h) (day (id β (id ββ f)) x y) (Z .Fβ g z) β‘β¨ day-ap (pullr (ap (_β h) (apβ _ββ_ refl (introl β.F-id)))) (day-glue id-comm-sym β day-ap refl (X .F-id #β x) refl) refl β©β‘ day (Ξ±β _ _ _ β (id ββ ((id ββ id) β h')) β h) (day id x (Y .Fβ f y)) (Z .Fβ g z) β assoc-from-cowedge : β i β Cowedge (Day-diagram X (Y βα΄° Z) i) assoc-from-cowedge i .nadir = Day.nadir (X βα΄° Y) Z i assoc-from-cowedge i .Ο (a , b) (h , x , y) = Day-rec (assoc-fromβ i h x) y assoc-from-cowedge i .extranatural (f , g) = ext Ξ» h x h' y z β day (Ξ±β _ _ _ β (id ββ h' β id) β (f ββ g) β h) (day id (X .Fβ id x) y) z β‘β¨ day-ap (ap (Ξ±β _ _ _ β_) (β.extendl (apβ _,_ id-comm-sym (ap (_β g) (idr h') β introl β.F-id)))) (day-ap refl (X .F-id #β _) refl) refl β©β‘ day (Ξ±β _ _ _ β (f ββ (id ββ id)) β (id ββ h' β g) β h) (day id x y) z β‘β¨ day-apβ (extendl (associator .IsoβΏ.from .is-natural _ _ _)) β©β‘ day (((f ββ id) ββ id) β Ξ±β _ _ _ β (id ββ h' β g) β h) (day id x y) z β‘β¨ day-glue refl β©β‘ day (Ξ±β _ _ _ β (id ββ h' β g) β h) (day (id β (f ββ id)) x y) (Z .Fβ id z) β‘β¨ day-ap (ap (Ξ±β _ _ _ β_) (apβ _β_ refl (introl β.F-id))) (day-glue id-comm-sym β day-ap refl refl (Y .F-id #β y)) (Z .F-id #β z) β©β‘ day (Ξ±β _ _ _ β (id ββ h' β g) β (id ββ id) β h) (day id (X .Fβ f x) y) z β Day-assoc : (X βα΄° Y) βα΄° Z β βΏ X βα΄° (Y βα΄° Z) Day-assoc = to-natural-iso mk-assoc where mk-assoc : make-natural-iso ((X βα΄° Y) βα΄° Z) (X βα΄° (Y βα΄° Z)) mk-assoc .eta x = Day-rec (assoc-to-cowedge x) mk-assoc .inv x = Day-rec (assoc-from-cowedge x) mk-assoc .etaβinv x = ext Ξ» h x h' y z β day (Ξ±β _ _ _ β (id ββ id) β Ξ±β _ _ _ β (id ββ h') β h) x (day id y z) β‘β¨ day-apβ (pulll (elimr β.F-id) β cancell (associator .IsoβΏ.invl Ξ·β _)) β©β‘ day ((id ββ h') β h) x (day id y z) β‘β¨ day-glue refl β©β‘ day h (X .Fβ id x) (day (id β h') y z) β‘β¨ day-ap refl (X .F-id #β x) (day-apβ (idl h')) β©β‘ day h x (day h' y z) β mk-assoc .invβeta x = ext Ξ» h h' x y z β day (Ξ±β _ _ _ β (id ββ id) β Ξ±β _ _ _ β (h' ββ id) β h) (day id x y) z β‘β¨ day-apβ (pulll (elimr β.F-id) β cancell (associator .IsoβΏ.invr Ξ·β _)) β©β‘ day ((h' ββ id) β h) (day id x y) z β‘β¨ day-glue refl β©β‘ day h (day (id β h') x y) (Z .Fβ id z) β‘β¨ day-ap refl (day-apβ (idl h')) (Z .F-id #β z) β©β‘ day h (day h' x y) z β mk-assoc .natural x y f = ext Ξ» h h' x y z β day ((Ξ±β _ _ _ β (h' ββ id) β h) β f) x (day id y z) β‘β¨ day-ap (pullr (pullr refl)) refl refl β©β‘ day (Ξ±β _ _ _ β (h' ββ id) β h β f) x (day id y z) β private module M = Monoidal-category abstract day-triangle : β {A B : β PSh β C β} β Day-map (Day-idr A .IsoβΏ.to) idnt βnt Day-assoc A (γβ C Unit) B .IsoβΏ.from β‘ Day-map idnt (Day-idl B .IsoβΏ.to) day-triangle {A} {B} = ext Ξ» i h x h' y z β day (Ξ±β _ _ _ β (id ββ h') β h) (A .Fβ (Οβ β (id ββ y) β id) x) z β‘β¨ day-ap refl (apβ (A .Fβ) (ap (Οβ β_) (idr _)) refl) (sym (B .F-id #β z)) β©β‘ day (Ξ±β _ _ _ β (id ββ h') β h) (A .Fβ (Οβ β (id ββ y)) x) (B .Fβ id z) β‘β¨ sym (day-glue refl) β©β‘ day ((Οβ β (id ββ y) ββ id) β Ξ±β _ _ _ β (id ββ h') β h) x z β‘β¨ day-apβ (β.pushl (apβ _,_ refl (introl refl))) β©β‘ day ((Οβ ββ id) β ((id ββ y) ββ id) β Ξ±β _ _ _ β (id ββ h') β h) x z β‘β¨ day-apβ (apβ _β_ refl (extendl (sym (associator .IsoβΏ.from .is-natural _ _ _)))) β©β‘ day ((Οβ ββ id) β Ξ±β _ _ _ β (id ββ (y ββ id)) β (id ββ h') β h) x z β‘β¨ day-apβ (pulll triangle) β©β‘ day ((id ββ Ξ»β) β (id ββ (y ββ id)) β (id ββ h') β h) x z β‘β¨ day-apβ (pulll (sym (β.F-β _ _)) β pulll (sym (β.F-β _ _)) β ap (_β h) (apβ _ββ_ (eliml (eliml refl)) (pullr refl))) β©β‘ day ((id ββ (Ξ»β β (y ββ id) β h')) β h) x z β‘β¨ day-glue refl β©β‘ day h (A .Fβ id x) (B .Fβ (Ξ»β β (y ββ id) β h') z) β‘β¨ day-ap refl (A .F-id #β x) refl β©β‘ day h x (B .Fβ (Ξ»β β (y ββ id) β h') z) β day-pentagon : β {A B C D : β PSh β C β} β Day-map (Day-assoc A B C .IsoβΏ.from) idnt βnt Day-assoc A (B βα΄° C) D .IsoβΏ.from βnt Day-map idnt (Day-assoc B C D .IsoβΏ.from) β‘ Day-assoc (A βα΄° B) C D .IsoβΏ.from βnt Day-assoc A B (C βα΄° D) .IsoβΏ.from day-pentagon {D = D} = ext Ξ» i h a h' b h'' c d β let it = (Ξ±β _ _ _ ββ id) β Ξ±β _ _ _ β (id ββ Ξ±β _ _ _ β (id ββ h'') β h') β h β‘β¨ apβ _β_ refl (apβ _β_ refl (β.pushl (apβ _,_ (intror refl) refl))) β©β‘ (Ξ±β _ _ _ ββ id) β Ξ±β _ _ _ β (id ββ Ξ±β _ _ _) β (id ββ (id ββ h'') β h') β h β‘β¨ pulll refl β extendl (pullr refl β pentagon) β©β‘ Ξ±β _ _ _ β Ξ±β _ _ _ β (id ββ (id ββ h'') β h') β h β‘β¨ apβ _β_ refl (apβ _β_ refl (β.pushl (apβ _,_ (intror refl) refl))) β©β‘ Ξ±β _ _ _ β Ξ±β _ _ _ β (id ββ (id ββ h'')) β (id ββ h') β h β‘β¨ apβ _β_ refl (extendl (associator .IsoβΏ.from .is-natural _ _ _)) β©β‘ Ξ±β _ _ _ β ((id ββ id) ββ h'') β Ξ±β _ _ _ β (id ββ h') β h β‘β¨ apβ _β_ refl (apβ _β_ (ap (_ββ h'') β.F-id) refl) β©β‘ (Ξ±β _ _ _ β (id ββ h'') β Ξ±β _ _ _ β (id ββ h') β h) β in day (Ξ±β _ _ _ β (id ββ (Ξ±β _ _ _) β (id ββ h'') β h') β h) (day (Ξ±β _ _ _ β (id ββ id) β id) (day id a b) c) d β‘β¨ day-ap refl (day-ap (elimr (eliml β.F-id) β introl refl) refl refl) (sym (D .F-id #β d)) β©β‘ day (Ξ±β _ _ _ β (id ββ (Ξ±β _ _ _) β (id ββ h'') β h') β h) (day (id β Ξ±β _ _ _) (day id a b) c) (D .Fβ id d) β‘β¨ sym (day-glue refl) β©β‘ day ((Ξ±β _ _ _ ββ id) β Ξ±β _ _ _ β (id ββ (Ξ±β _ _ _) β (id ββ h'') β h') β h) (day id (day id a b) c) d β‘β¨ day-apβ it β©β‘ day (Ξ±β _ _ _ β (id ββ h'') β Ξ±β _ _ _ β (id ββ h') β h) (day id (day id a b) c) d β Day-monoidal : Monoidal-category (PSh β C) Day-monoidal .M.-β- = Day-bifunctor Day-monoidal .M.Unit = γβ C Unit Day-monoidal .M.unitor-l = to-natural-iso mk-Ξ» where mk-Ξ» : make-natural-iso _ _ mk-Ξ» .eta x = Day-idl x .IsoβΏ.from mk-Ξ» .inv x = Day-idl x .IsoβΏ.to mk-Ξ» .etaβinv x = Day-idl x .IsoβΏ.invr mk-Ξ» .invβeta x = Day-idl x .IsoβΏ.invl mk-Ξ» .natural x y f = trivial! Day-monoidal .M.unitor-r = to-natural-iso mk-Ο where mk-Ο : make-natural-iso _ _ mk-Ο .eta x = Day-idr x .IsoβΏ.from mk-Ο .inv x = Day-idr x .IsoβΏ.to mk-Ο .etaβinv x = Day-idr x .IsoβΏ.invr mk-Ο .invβeta x = Day-idr x .IsoβΏ.invl mk-Ο .natural x y f = trivial! Day-monoidal .M.associator = to-natural-iso mk-Ξ± where mk-Ξ± : make-natural-iso _ _ mk-Ξ± .eta (x , y , z) = Day-assoc x y z .IsoβΏ.to mk-Ξ± .inv (x , y , z) = Day-assoc x y z .IsoβΏ.from mk-Ξ± .etaβinv (x , y , z) = Day-assoc x y z .IsoβΏ.invl mk-Ξ± .invβeta (x , y , z) = Day-assoc x y z .IsoβΏ.invr mk-Ξ± .natural x y f = trivial! Day-monoidal .M.triangle {A} {B} = day-triangle Day-monoidal .M.pentagon {A} {B} {C} {D} = day-pentagon
This is actually a slight under-approximation of strong monoidal functors: the unit must also be preserved, of course, and the preservation isomorphisms need to be compatible with the structural morphisms β the unitors and associator.β©οΈ