module Cat.Monoidal.Instances.Factorisations {o ℓ} (C : Precategory o ℓ) where
private Ff = Factorisations C open Cat.Reasoning C open Factorisation using (elim ; collapse ; weave ; adjust) open Make-bifunctor
Monoidal structure on functorial factorisations🔗
We show how to equip the category of functorial factorisations on with the structure of a monoidal category, such that a monoid on some factorisation is precisely a right weak factorisation structure on
The unit factorisation sends each to
Ff-unit : Factorisation C Ff-unit .S₀ (_ , _ , f) = record { left = id ; right = f ; factors = intror refl } Ff-unit .S₁ f = record { sq₀ = id-comm-sym ; sq₁ = f .com } Ff-unit .S-id = ext refl Ff-unit .S-∘ f g = ext refl
We can easily calculate that this unit factorisation is initial.
Ff-unit-is-initial : is-initial (Factorisations C) Ff-unit
Ff-unit-is-initial other = record where module o = Factorisation other centre = record { map = λ (X , Y , f) → record { map = o.λ→ f ; sq₀ = refl ; sq₁ = sym (o.factors f) ∙ introl refl } ; com = λ x y f → Interpolant-pathp (other .S₁ f .sq₀) } paths h = ext λ x y f → o.λ→ f ≡⟨ h .sq₀ᶠᶠ f ⟩≡ h .mapᶠᶠ f ∘ id ≡⟨ elimr refl ⟩≡ h .mapᶠᶠ f ∎
If are a pair of factorisations, their tensor sends a map to the composite with “middle object” i.e. everything but the last arrow is the left factor.
module _ (F G : Factorisation C) where private module F = Factorisation F module G = Factorisation G _⊗ᶠᶠ_ : Factorisation C _⊗ᶠᶠ_ .S₀ (_ , _ , f) = record where mid = G.Mid₀ (F.ρ→ f) left = G.λ→ (F.ρ→ f) ∘ F.λ→ f right = G.ρ→ (F.ρ→ f) factors = sym (pulll (sym (G.factors _)) ∙ sym (F.factors _)) _⊗ᶠᶠ_ .S₁ sq = record where open Interpolant (G .S₁ record { com = S₁ F sq .sq₁ }) using (sq₁ ; map) renaming (sq₀ to α) sq₀ = sym (pulll (sym α) ∙ extendr (sym (F .S₁ sq .sq₀))) _⊗ᶠᶠ_ .S-id = ext (G.elim (ext (F.elim refl ,ₚ refl))) _⊗ᶠᶠ_ .S-∘ f g = ext (G.expand (ext (F.expand refl ,ₚ refl)))
Showing that this extends to a functor is slightly annoying, but unsurprising.
Ff-tensor-functor : Bifunctor Ff Ff Ff Ff-tensor-functor = make-bifunctor mk where mk : Make-bifunctor mk .F₀ F F' = F ⊗ᶠᶠ F' mk .lmap {x = X} f .map (_ , _ , h) = let sq = record { com = f .sq₁ᶠᶠ h ∙ introl refl } in record { map = X .S₁ sq .map ; sq₀ = sym (pulll (sym (X .S₁ sq .sq₀)) ∙ pullr (sym (f .sq₀ᶠᶠ h)) ∙ intror refl) ; sq₁ = X .S₁ sq .sq₁ } mk .lmap {x = X} f .com x y g = Interpolant-pathp (weave X (ext (f .comᶠᶠ _ ,ₚ id-comm-sym))) mk .rmap {a = A} g .map (_ , _ , h) = record { map = g .mapᶠᶠ (Factorisation.ρ→ A h) ; sq₀ = elimr refl ∙ sym (pulll (sym (g .sq₀ᶠᶠ _))) ; sq₁ = g .map _ .sq₁ } mk .rmap g .com x y f = Interpolant-pathp (g .comᶠᶠ _) mk .lmap-id {x = X} = ext λ x y h → elim X (ext refl) mk .lmap-∘ {x = X} f g = ext λ x y h → sym (collapse X (ext (refl ,ₚ idr id))) mk .rmap-id = ext λ x y h → refl mk .rmap-∘ f g = ext λ x y h → refl mk .lrmap f g = ext λ x y h → sym (g .comᶠᶠ _)
The following snippet, showing part of the construction of the associator, is typical of the construction of the monoidal structure on every component of the natural isomorphisms is the identity, but we end up having to shuffle quite a few identity morphisms around.
private assc : Associator-for {O = ⊤} (λ _ _ → Ff) Ff-tensor-functor assc = to-natural-iso mk where mk : make-natural-iso (compose-assocˡ (λ _ _ → Ff) Ff-tensor-functor) _ mk .eta X .map x = record { map = id ; sq₀ = elimr refl ∙∙ pullr refl ∙∙ introl refl ; sq₁ = id-comm } mk .inv X .map x = record { map = id ; sq₀ = elimr refl ∙∙ pulll refl ∙∙ introl refl ; sq₁ = id-comm }
mk .eta X .com x y f = Interpolant-pathp id-comm-sym mk .inv X .com x y f = Interpolant-pathp id-comm-sym mk .eta∘inv x = ext λ x y f → idl id mk .inv∘eta x = ext λ x y f → idl id mk .natural (X , X') (Y , Y') f = ext λ x y h → pullr (elimr refl) ∙∙ pulll (Factorisation.collapse (Y' .snd) (ext (refl ,ₚ idl id))) ∙∙ introl refl
Ff-monoidal : Monoidal-category Ff
Ff-monoidal .-⊗- = Ff-tensor-functor
Ff-monoidal .Unit = Ff-unit
We thus choose not to comment much on the construction of the unitors
and proof of the triangle and pentagon identities.
Ff-monoidal .unitor-l = to-natural-iso mk where mk : make-natural-iso (Id {C = Ff}) (Bifunctor.Right Ff-tensor-functor Ff-unit) mk .eta X .map _ = record { sq₀ = cancelr (idl id) ∙ introl refl ; sq₁ = id-comm } mk .inv X .map _ = record { sq₀ = introl refl ; sq₁ = id-comm } mk .eta X .com x y f = Interpolant-pathp $ eliml refl ∙∙ adjust X (ext refl) ∙∙ intror refl mk .inv X .com x y f = Interpolant-pathp $ eliml refl ∙∙ adjust X (ext refl) ∙∙ intror refl mk .eta∘inv x = ext λ x y f → idl id mk .inv∘eta x = ext λ x y f → idl id mk .natural X Y f = ext λ x y g → id-comm Ff-monoidal .unitor-r = to-natural-iso mk where mk : make-natural-iso (Id {C = Ff}) (Bifunctor.Left Ff-tensor-functor Ff-unit) mk .eta X .map _ = record { sq₀ = elimr refl ; sq₁ = id-comm } mk .inv X .map _ = record { sq₀ = elimr refl ∙ insertl (idl id) ; sq₁ = id-comm } mk .eta X .com x y f = Interpolant-pathp $ eliml refl ∙∙ Factorisation.adjust X (ext refl) ∙∙ intror refl mk .inv X .com x y f = Interpolant-pathp $ eliml refl ∙∙ Factorisation.adjust X (ext refl) ∙∙ intror refl mk .eta∘inv x = ext λ x y f → idl id mk .inv∘eta x = ext λ x y f → idl id mk .natural X Y f = ext λ x y g → id-comm Ff-monoidal .associator = assc Ff-monoidal .triangle {B = B} = ext λ x y f → elimr refl ∙ elim B (ext refl) Ff-monoidal .pentagon {B = B} {C = C} {D = D} = ext λ x y f → eliml (elim D (ext refl))
Monoids on functorial factorisations🔗
module _ {F : Factorisation C} (m : Monoid-on Ff-monoidal F) where private module m = Monoid-on m module F = Factorisation F open is-monad open Rwfs-on
We will now show that a monoid (on some functorial factorisation in this monoidal structure can be tweaked into a right weak factorisation structure on First, note that the components of the monoidal multiplication on can be reassembled into a monadic multiplication on the right factor.
private monoid→mult : F.R F∘ F.R => F.R monoid→mult .η (X , Y , f) = record where top = m.μ .mapᶠᶠ f bot = id com = m.μ .sq₁ᶠᶠ f ∙ introl refl monoid→mult .is-natural x y f = ext $ ap₂ _∘_ refl (F.adjust (ext refl)) ∙ m.μ .comᶠᶠ _ ,ₚ id-comm-sym
For ease of calculation below, we can also extract a unit
map from the monoid structure on
monoid→unit : Id => F.R
monoid-unit-agrees : monoid→unit ≡ F.R-η
Of course, what we need to show is that the monoid multiplication makes
the right factor
functor
with its canonical unit
into a monad. However, that the unit derived from the monoid agrees with
is an easy corollary of initiality for the unit factorisation.
monoid→unit .η (X , Y , f) = record { top = m.η .mapᶠᶠ f ; bot = id ; com = m.η .sq₁ᶠᶠ f ∙ introl refl } monoid→unit .is-natural x y f = ext (m.η .comᶠᶠ _ ,ₚ id-comm-sym) monoid-unit-agrees = ext λ (x , y , f) → intror refl ∙ sym (m.η .sq₀ᶠᶠ f) ,ₚ refl
The calculation that these two are a monad on is a straightforward repackaging of the corresponding monoid laws.
monoid-mult-is-monad : is-monad monoid→unit monoid→mult monoid-mult-is-monad .μ-unitr {X , Y , f} = ext $ cdr (F.adjust (ext refl)) ∙ apd (λ i x → x .mapᶠᶠ f) m.μ-unitl ,ₚ idl id monoid-mult-is-monad .μ-unitl {X , Y , f} = ext $ apd (λ i x → x .mapᶠᶠ f) m.μ-unitr ,ₚ idl id monoid-mult-is-monad .μ-assoc {X , Y , f} = ext $ cdr (F.adjust (ext refl) ∙ intror refl) ∙ apd (λ i x → x .mapᶠᶠ f) (sym m.μ-assoc) ,ₚ refl
We can then transport this along the proof that the units agree to extend to a monad. This transport will not compute very nicely, but since “being a monad” is a proposition once the unit and multiplication are fixed, this does not matter.
monoid-on→rwfs-on : Rwfs-on F monoid-on→rwfs-on .R-μ = monoid→mult monoid-on→rwfs-on .R-monad = done where abstract done : is-monad F.R-η monoid→mult done = subst (λ e → is-monad e monoid→mult) monoid-unit-agrees monoid-mult-is-monad