The precategory of functors and natural transformations between two precategories
Content created by Fredrik Bakke, Jonathan Prieto-Cubides, Egbert Rijke and Daniel Gratzer.
Created on 2023-01-16.
Last modified on 2023-09-27.
module category-theory.precategory-of-functors where
Imports
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.propositions open import foundation.universe-levels
Idea
Functors between precategories and natural transformations 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
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 associative-composition-structure-functor-precategory-Precategory : associative-composition-structure-Set ( natural-transformation-set-Precategory C D) pr1 associative-composition-structure-functor-precategory-Precategory {F} {G} {H} = comp-hom-functor-precategory-Precategory {F} {G} {H} pr2 associative-composition-structure-functor-precategory-Precategory {F} {G} {H} {I} = associative-comp-hom-functor-precategory-Precategory {F} {G} {H} {I} 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-structure-functor-precategory-Precategory : is-unital-composition-structure-Set ( natural-transformation-set-Precategory C D) ( associative-composition-structure-functor-precategory-Precategory) pr1 is-unital-composition-structure-functor-precategory-Precategory = id-hom-functor-precategory-Precategory pr1 ( pr2 is-unital-composition-structure-functor-precategory-Precategory) { F} {G} = left-unit-law-comp-hom-functor-precategory-Precategory {F} {G} pr2 ( pr2 is-unital-composition-structure-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-structure-functor-precategory-Precategory pr2 (pr2 (pr2 functor-precategory-Precategory)) = is-unital-composition-structure-functor-precategory-Precategory
Properties
Isomorphisms in the functor precategory are natural isomorphisms
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-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-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
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
Recent changes
- 2023-09-27. Fredrik Bakke. Presheaf categories (#801).
- 2023-09-26. Fredrik Bakke and Egbert Rijke. Maps of categories, functor categories, and small subprecategories (#794).
- 2023-09-15. Fredrik Bakke. Define representations of monoids (#765).
- 2023-05-06. Egbert Rijke. Big cleanup throughout library (#594).
- 2023-05-01. Fredrik Bakke. Refactor 2, the sequel to refactor (#581).