module Cat.Instances.Functor.Compose where
Functoriality of functor compositionπ
When the operation of functor composition, , is seen as happening not only to functors but to whole functor categories, then it is itself functorial. This is a bit mind-bending at first, but this module will construct the functor composition functors. Thereβs actually a family of three related functors weβre interested in:
- The functor composition functor itself, having type ;
- The precomposition functor associated with any , which will be denoted in TeX and precompose in Agda;
- The postcomposition functor associated with any , which will be denoted ; In the code, thatβs postcompose.
Note that the precomposition functor is necessarily βcontravariantβ when compared with , in that it points in the opposite direction to .
private variable o β : Level A B C Cβ² D E : Precategory o β F G H K : Functor C D Ξ± Ξ² Ξ³ : F => G
Fβ-functor : Functor (Cat[ B , C ] ΓαΆ Cat[ A , B ]) Cat[ A , C ] Fβ-functor {C = C} = go module Fβ-f where private module C = Cat.Reasoning C go : Functor _ _ go .Fβ (F , G) = F Fβ G go .Fβ {y = y , _} (n1 , n2) .Ξ· x = y .Fβ (n2 .Ξ· _) C.β n1 .Ξ· _ go .Fβ {x = F , G} {y = W , X} (n1 , n2) .is-natural _ _ f = (W .Fβ (n2 .Ξ· _) C.β n1 .Ξ· _) C.β F .Fβ (G .Fβ f) β‘β¨ C.pullr (n1 .is-natural _ _ _) β©β‘ W .Fβ (n2 .Ξ· _) C.β W .Fβ (G .Fβ f) C.β n1 .Ξ· _ β‘β¨ C.extendl (W.weave (n2 .is-natural _ _ _)) β©β‘ W .Fβ (X .Fβ f) C.β W .Fβ (n2 .Ξ· _) C.β n1 .Ξ· _ β where module W = Fr W go .F-id {x} = Nat-path Ξ» _ β C.idr _ β x .fst .F-id go .F-β {x} {y , _} {z , _} (f , _) (g , _) = Nat-path Ξ» _ β z .Fβ _ C.β f .Ξ· _ C.β g .Ξ· _ β‘β¨ C.pushl (z .F-β _ _) β©β‘ z .Fβ _ C.β z .Fβ _ C.β f .Ξ· _ C.β g .Ξ· _ β‘β¨ C.extend-inner (sym (f .is-natural _ _ _)) β©β‘ z .Fβ _ C.β f .Ξ· _ C.β y .Fβ _ C.β g .Ξ· _ β‘β¨ C.pulll refl β©β‘ (z .Fβ _ C.β f .Ξ· _) C.β (y .Fβ _ C.β g .Ξ· _) β {-# DISPLAY Fβ-f.go = Fβ-functor #-}
Before setting up the pre/post-composition functors, we define their action on morphisms (natural transformations) first, called whiskerings, first. The mnemonic for triangles is that the base points towards the side that does not change, so in (e.g.) , the is unchanging: this expression has type , as long as .
_β_ : F => G β (H : Functor C D) β F Fβ H => G Fβ H _β_ nt H .Ξ· x = nt .Ξ· _ _β_ nt H .is-natural x y f = nt .is-natural _ _ _ _βΈ_ : (H : Functor E C) β F => G β H Fβ F => H Fβ G _βΈ_ H nt .Ξ· x = H .Fβ (nt .Ξ· x) _βΈ_ H nt .is-natural x y f = sym (H .F-β _ _) β ap (H .Fβ) (nt .is-natural _ _ _) β H .F-β _ _
With the whiskerings already defined, defining and is easy:
module _ (p : Functor C Cβ²) where precompose : Functor Cat[ Cβ² , D ] Cat[ C , D ] precompose .Fβ G = G Fβ p precompose .Fβ ΞΈ = ΞΈ β p precompose .F-id = Nat-path Ξ» _ β refl precompose .F-β f g = Nat-path Ξ» _ β refl postcompose : Functor Cat[ D , C ] Cat[ D , Cβ² ] postcompose .Fβ G = p Fβ G postcompose .Fβ ΞΈ = p βΈ ΞΈ postcompose .F-id = Nat-path Ξ» _ β p .F-id postcompose .F-β f g = Nat-path Ξ» _ β p .F-β _ _
Whiskerings are instances of a more general form of composition for natural transformations, known as horizontal composition.
_β_ : β {F G : Functor D E} {H K : Functor C D} β F => G β H => K β F Fβ H => G Fβ K _β_ {E = E} {F = F} {G} {H} {K} Ξ± Ξ² = nat module horizontal-comp where private module E = Cat.Reasoning E open Fr nat : F Fβ H => G Fβ K nat .Ξ· x = G .Fβ (Ξ² .Ξ· _) E.β Ξ± .Ξ· _ nat .is-natural x y f = E.pullr (Ξ± .is-natural _ _ _) β E.extendl (weave G (Ξ² .is-natural _ _ _))
module _ {F G : Functor C D} where open Cat.Morphism open Fr _βni_ : natural-iso F G β (H : Functor B C) β natural-iso (F Fβ H) (G Fβ H) (Ξ± βni H) = make-iso _ (Ξ± .to β H) (Ξ± .from β H) (Nat-path Ξ» _ β Ξ± .invl Ξ·β _) (Nat-path Ξ» _ β Ξ± .invr Ξ·β _) _βΈni_ : (H : Functor D E) β natural-iso F G β natural-iso (H Fβ F) (H Fβ G) (H βΈni Ξ±) = make-iso _ (H βΈ Ξ± .to) (H βΈ Ξ± .from) (Nat-path Ξ» _ β annihilate H (Ξ± .invl Ξ·β _)) (Nat-path Ξ» _ β annihilate H (Ξ± .invr Ξ·β _))