# The precategory of functors and natural transformations between two precategories ```agda module category-theory.precategory-of-functors where ``` <details><summary>Imports</summary> ```agda open import category-theory.composition-operations-on-binary-families-of-sets open import category-theory.functors-precategories open import category-theory.isomorphisms-in-precategories open import category-theory.natural-isomorphisms-functors-precategories open import category-theory.natural-transformations-functors-precategories open import category-theory.precategories open import foundation.action-on-identifications-functions open import foundation.dependent-pair-types open import foundation.equivalences open import foundation.function-extensionality open import foundation.functoriality-dependent-pair-types open import foundation.identity-types open import foundation.logical-equivalences open import foundation.propositions open import foundation.strictly-involutive-identity-types open import foundation.universe-levels ``` </details> ## Idea [Functors](category-theory.functors-precategories.md) between [precategories](category-theory.precategories.md) and [natural transformations](category-theory.natural-transformations-functors-precategories.md) between them introduce a new precategory whose identity map and composition structure are inherited pointwise from the codomain precategory. This is called the **precategory of functors**. ## Definitions ### The precategory of functors and natural transformations between precategories ```agda module _ {l1 l2 l3 l4 : Level} (C : Precategory l1 l2) (D : Precategory l3 l4) where comp-hom-functor-precategory-Precategory : {F G H : functor-Precategory C D} → natural-transformation-Precategory C D G H → natural-transformation-Precategory C D F G → natural-transformation-Precategory C D F H comp-hom-functor-precategory-Precategory {F} {G} {H} = comp-natural-transformation-Precategory C D F G H associative-comp-hom-functor-precategory-Precategory : {F G H I : functor-Precategory C D} (h : natural-transformation-Precategory C D H I) (g : natural-transformation-Precategory C D G H) (f : natural-transformation-Precategory C D F G) → comp-natural-transformation-Precategory C D F G I ( comp-natural-transformation-Precategory C D G H I h g) ( f) = comp-natural-transformation-Precategory C D F H I ( h) ( comp-natural-transformation-Precategory C D F G H g f) associative-comp-hom-functor-precategory-Precategory {F} {G} {H} {I} h g f = associative-comp-natural-transformation-Precategory C D F G H I f g h involutive-eq-associative-comp-hom-functor-precategory-Precategory : {F G H I : functor-Precategory C D} (h : natural-transformation-Precategory C D H I) (g : natural-transformation-Precategory C D G H) (f : natural-transformation-Precategory C D F G) → comp-natural-transformation-Precategory C D F G I ( comp-natural-transformation-Precategory C D G H I h g) ( f) =ⁱ comp-natural-transformation-Precategory C D F H I ( h) ( comp-natural-transformation-Precategory C D F G H g f) involutive-eq-associative-comp-hom-functor-precategory-Precategory { F} {G} {H} {I} h g f = involutive-eq-associative-comp-natural-transformation-Precategory C D F G H I f g h associative-composition-operation-functor-precategory-Precategory : associative-composition-operation-binary-family-Set ( natural-transformation-set-Precategory C D) pr1 associative-composition-operation-functor-precategory-Precategory {F} {G} {H} = comp-hom-functor-precategory-Precategory {F} {G} {H} pr2 associative-composition-operation-functor-precategory-Precategory { F} {G} {H} {I} h g f = involutive-eq-associative-comp-hom-functor-precategory-Precategory { F} {G} {H} {I} h g f id-hom-functor-precategory-Precategory : (F : functor-Precategory C D) → natural-transformation-Precategory C D F F id-hom-functor-precategory-Precategory = id-natural-transformation-Precategory C D left-unit-law-comp-hom-functor-precategory-Precategory : {F G : functor-Precategory C D} (α : natural-transformation-Precategory C D F G) → comp-natural-transformation-Precategory C D F G G ( id-natural-transformation-Precategory C D G) α = α left-unit-law-comp-hom-functor-precategory-Precategory {F} {G} = left-unit-law-comp-natural-transformation-Precategory C D F G right-unit-law-comp-hom-functor-precategory-Precategory : {F G : functor-Precategory C D} (α : natural-transformation-Precategory C D F G) → comp-natural-transformation-Precategory C D F F G α (id-natural-transformation-Precategory C D F) = α right-unit-law-comp-hom-functor-precategory-Precategory {F} {G} = right-unit-law-comp-natural-transformation-Precategory C D F G is-unital-composition-operation-functor-precategory-Precategory : is-unital-composition-operation-binary-family-Set ( natural-transformation-set-Precategory C D) ( λ {F} {G} {H} → comp-hom-functor-precategory-Precategory {F} {G} {H}) pr1 is-unital-composition-operation-functor-precategory-Precategory = id-hom-functor-precategory-Precategory pr1 ( pr2 is-unital-composition-operation-functor-precategory-Precategory) { F} {G} = left-unit-law-comp-hom-functor-precategory-Precategory {F} {G} pr2 ( pr2 is-unital-composition-operation-functor-precategory-Precategory) { F} {G} = right-unit-law-comp-hom-functor-precategory-Precategory {F} {G} functor-precategory-Precategory : Precategory (l1 ⊔ l2 ⊔ l3 ⊔ l4) (l1 ⊔ l2 ⊔ l4) pr1 functor-precategory-Precategory = functor-Precategory C D pr1 (pr2 functor-precategory-Precategory) = natural-transformation-set-Precategory C D pr1 (pr2 (pr2 functor-precategory-Precategory)) = associative-composition-operation-functor-precategory-Precategory pr2 (pr2 (pr2 functor-precategory-Precategory)) = is-unital-composition-operation-functor-precategory-Precategory ``` ## Properties ### Isomorphisms in the functor precategory are natural isomorphisms ```agda module _ {l1 l2 l3 l4 : Level} (C : Precategory l1 l2) (D : Precategory l3 l4) (F G : functor-Precategory C D) where is-iso-functor-is-natural-isomorphism-Precategory : (f : natural-transformation-Precategory C D F G) → is-natural-isomorphism-Precategory C D F G f → is-iso-Precategory (functor-precategory-Precategory C D) {F} {G} f pr1 (is-iso-functor-is-natural-isomorphism-Precategory f is-iso-f) = natural-transformation-inv-is-natural-isomorphism-Precategory C D F G f is-iso-f pr1 (pr2 (is-iso-functor-is-natural-isomorphism-Precategory f is-iso-f)) = is-section-natural-transformation-inv-is-natural-isomorphism-Precategory C D F G f is-iso-f pr2 (pr2 (is-iso-functor-is-natural-isomorphism-Precategory f is-iso-f)) = is-retraction-natural-transformation-inv-is-natural-isomorphism-Precategory C D F G f is-iso-f is-natural-isomorphism-is-iso-functor-Precategory : (f : natural-transformation-Precategory C D F G) → is-iso-Precategory (functor-precategory-Precategory C D) {F} {G} f → is-natural-isomorphism-Precategory C D F G f pr1 (is-natural-isomorphism-is-iso-functor-Precategory f is-iso-f x) = hom-family-natural-transformation-Precategory C D G F ( hom-inv-is-iso-Precategory ( functor-precategory-Precategory C D) {F} {G} is-iso-f) ( x) pr1 (pr2 (is-natural-isomorphism-is-iso-functor-Precategory f is-iso-f x)) = htpy-eq ( ap ( hom-family-natural-transformation-Precategory C D G G) ( is-section-hom-inv-is-iso-Precategory ( functor-precategory-Precategory C D) {F} {G} is-iso-f)) ( x) pr2 (pr2 (is-natural-isomorphism-is-iso-functor-Precategory f is-iso-f x)) = htpy-eq ( ap ( hom-family-natural-transformation-Precategory C D F F) ( is-retraction-hom-inv-is-iso-Precategory ( functor-precategory-Precategory C D) {F} {G} is-iso-f)) ( x) is-equiv-is-iso-functor-is-natural-isomorphism-Precategory : (f : natural-transformation-Precategory C D F G) → is-equiv (is-iso-functor-is-natural-isomorphism-Precategory f) is-equiv-is-iso-functor-is-natural-isomorphism-Precategory f = is-equiv-has-converse-is-prop ( is-prop-is-natural-isomorphism-Precategory C D F G f) ( is-prop-is-iso-Precategory ( functor-precategory-Precategory C D) {F} {G} f) ( is-natural-isomorphism-is-iso-functor-Precategory f) is-equiv-is-natural-isomorphism-is-iso-functor-Precategory : (f : natural-transformation-Precategory C D F G) → is-equiv (is-natural-isomorphism-is-iso-functor-Precategory f) is-equiv-is-natural-isomorphism-is-iso-functor-Precategory f = is-equiv-has-converse-is-prop ( is-prop-is-iso-Precategory ( functor-precategory-Precategory C D) {F} {G} f) ( is-prop-is-natural-isomorphism-Precategory C D F G f) ( is-iso-functor-is-natural-isomorphism-Precategory f) equiv-is-iso-functor-is-natural-isomorphism-Precategory : (f : natural-transformation-Precategory C D F G) → is-natural-isomorphism-Precategory C D F G f ≃ is-iso-Precategory (functor-precategory-Precategory C D) {F} {G} f pr1 (equiv-is-iso-functor-is-natural-isomorphism-Precategory f) = is-iso-functor-is-natural-isomorphism-Precategory f pr2 (equiv-is-iso-functor-is-natural-isomorphism-Precategory f) = is-equiv-is-iso-functor-is-natural-isomorphism-Precategory f equiv-is-natural-isomorphism-is-iso-functor-Precategory : (f : natural-transformation-Precategory C D F G) → is-iso-Precategory (functor-precategory-Precategory C D) {F} {G} f ≃ is-natural-isomorphism-Precategory C D F G f pr1 (equiv-is-natural-isomorphism-is-iso-functor-Precategory f) = is-natural-isomorphism-is-iso-functor-Precategory f pr2 (equiv-is-natural-isomorphism-is-iso-functor-Precategory f) = is-equiv-is-natural-isomorphism-is-iso-functor-Precategory f iso-functor-natural-isomorphism-Precategory : natural-isomorphism-Precategory C D F G → iso-Precategory (functor-precategory-Precategory C D) F G iso-functor-natural-isomorphism-Precategory = tot is-iso-functor-is-natural-isomorphism-Precategory natural-isomorphism-iso-functor-Precategory : iso-Precategory (functor-precategory-Precategory C D) F G → natural-isomorphism-Precategory C D F G natural-isomorphism-iso-functor-Precategory = tot is-natural-isomorphism-is-iso-functor-Precategory is-equiv-iso-functor-natural-isomorphism-Precategory : is-equiv iso-functor-natural-isomorphism-Precategory is-equiv-iso-functor-natural-isomorphism-Precategory = is-equiv-tot-is-fiberwise-equiv is-equiv-is-iso-functor-is-natural-isomorphism-Precategory is-equiv-natural-isomorphism-iso-functor-Precategory : is-equiv natural-isomorphism-iso-functor-Precategory is-equiv-natural-isomorphism-iso-functor-Precategory = is-equiv-tot-is-fiberwise-equiv is-equiv-is-natural-isomorphism-is-iso-functor-Precategory equiv-iso-functor-natural-isomorphism-Precategory : natural-isomorphism-Precategory C D F G ≃ iso-Precategory (functor-precategory-Precategory C D) F G equiv-iso-functor-natural-isomorphism-Precategory = equiv-tot equiv-is-iso-functor-is-natural-isomorphism-Precategory equiv-natural-isomorphism-iso-functor-Precategory : iso-Precategory (functor-precategory-Precategory C D) F G ≃ natural-isomorphism-Precategory C D F G equiv-natural-isomorphism-iso-functor-Precategory = equiv-tot equiv-is-natural-isomorphism-is-iso-functor-Precategory ``` #### Computing with the equivalence that isomorphisms are natural isomorphisms ```agda module _ {l1 l2 l3 l4 : Level} (C : Precategory l1 l2) (D : Precategory l3 l4) (F G : functor-Precategory C D) where compute-iso-functor-natural-isomorphism-eq-Precategory : (p : F = G) → iso-eq-Precategory (functor-precategory-Precategory C D) F G p = iso-functor-natural-isomorphism-Precategory C D F G ( natural-isomorphism-eq-Precategory C D F G p) compute-iso-functor-natural-isomorphism-eq-Precategory refl = eq-iso-eq-hom-Precategory ( functor-precategory-Precategory C D) { F} {G} _ _ refl ``` ### The evaluation functor ```agda module _ {l1 l2 l3 l4 : Level} (C : Precategory l1 l2) (D : Precategory l3 l4) where ev-functor-Precategory : (c : obj-Precategory C) → functor-Precategory (functor-precategory-Precategory C D) D pr1 (ev-functor-Precategory c) F = obj-functor-Precategory C D F c pr1 (pr2 (ev-functor-Precategory c)) {F} {G} φ = hom-family-natural-transformation-Precategory C D F G φ c pr1 (pr2 (pr2 (ev-functor-Precategory c))) φ Ψ = refl pr2 (pr2 (pr2 (ev-functor-Precategory c))) F = refl ```