Natural transformations between functors between precategories
Content created by Fredrik Bakke.
Created on 2023-09-27.
Last modified on 2023-11-27.
module category-theory.natural-transformations-functors-precategories where
Imports
open import category-theory.functors-precategories open import category-theory.natural-transformations-maps-precategories open import category-theory.precategories open import foundation.dependent-pair-types open import foundation.embeddings open import foundation.equivalences open import foundation.homotopies open import foundation.identity-types open import foundation.propositions open import foundation.sets open import foundation.universe-levels
Idea
Given precategories C
and D
, a natural
transformation from a functor
F : C → D
to G : C → D
consists of :
- a family of morphisms
γ : (x : C) → hom (F x) (G x)
such that the following identity holds: (G f) ∘ (γ x) = (γ y) ∘ (F f)
, for allf : hom x y
.
Definition
module _ {l1 l2 l3 l4 : Level} (C : Precategory l1 l2) (D : Precategory l3 l4) (F G : functor-Precategory C D) where hom-family-functor-Precategory : UU (l1 ⊔ l4) hom-family-functor-Precategory = hom-family-map-Precategory C D ( map-functor-Precategory C D F) ( map-functor-Precategory C D G) is-natural-transformation-Precategory : hom-family-functor-Precategory → UU (l1 ⊔ l2 ⊔ l4) is-natural-transformation-Precategory = is-natural-transformation-map-Precategory C D ( map-functor-Precategory C D F) ( map-functor-Precategory C D G) natural-transformation-Precategory : UU (l1 ⊔ l2 ⊔ l4) natural-transformation-Precategory = natural-transformation-map-Precategory C D ( map-functor-Precategory C D F) ( map-functor-Precategory C D G) hom-family-natural-transformation-Precategory : natural-transformation-Precategory → hom-family-functor-Precategory hom-family-natural-transformation-Precategory = hom-family-natural-transformation-map-Precategory C D ( map-functor-Precategory C D F) ( map-functor-Precategory C D G) naturality-natural-transformation-Precategory : (γ : natural-transformation-Precategory) → is-natural-transformation-Precategory ( hom-family-natural-transformation-Precategory γ) naturality-natural-transformation-Precategory = naturality-natural-transformation-map-Precategory C D ( map-functor-Precategory C D F) ( map-functor-Precategory C D G)
Composition and identity of natural transformations
module _ {l1 l2 l3 l4 : Level} (C : Precategory l1 l2) (D : Precategory l3 l4) where id-natural-transformation-Precategory : (F : functor-Precategory C D) → natural-transformation-Precategory C D F F id-natural-transformation-Precategory F = id-natural-transformation-map-Precategory C D ( map-functor-Precategory C D F) comp-natural-transformation-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-natural-transformation-Precategory F G H = comp-natural-transformation-map-Precategory C D ( map-functor-Precategory C D F) ( map-functor-Precategory C D G) ( map-functor-Precategory C D H)
Properties
That a family of morphisms is a natural transformation is a proposition
This follows from the fact that the hom-types are sets.
module _ {l1 l2 l3 l4 : Level} (C : Precategory l1 l2) (D : Precategory l3 l4) (F G : functor-Precategory C D) where is-prop-is-natural-transformation-Precategory : (γ : hom-family-functor-Precategory C D F G) → is-prop (is-natural-transformation-Precategory C D F G γ) is-prop-is-natural-transformation-Precategory = is-prop-is-natural-transformation-map-Precategory C D ( map-functor-Precategory C D F) ( map-functor-Precategory C D G) is-natural-transformation-prop-Precategory : (γ : hom-family-functor-Precategory C D F G) → Prop (l1 ⊔ l2 ⊔ l4) is-natural-transformation-prop-Precategory = is-natural-transformation-prop-map-Precategory C D ( map-functor-Precategory C D F) ( map-functor-Precategory C D G)
The set of natural transformations
module _ {l1 l2 l3 l4 : Level} (C : Precategory l1 l2) (D : Precategory l3 l4) (F G : functor-Precategory C D) where is-emb-hom-family-natural-transformation-Precategory : is-emb (hom-family-natural-transformation-Precategory C D F G) is-emb-hom-family-natural-transformation-Precategory = is-emb-hom-family-natural-transformation-map-Precategory C D ( map-functor-Precategory C D F) ( map-functor-Precategory C D G) emb-hom-family-natural-transformation-Precategory : natural-transformation-Precategory C D F G ↪ hom-family-functor-Precategory C D F G emb-hom-family-natural-transformation-Precategory = emb-hom-family-natural-transformation-map-Precategory C D ( map-functor-Precategory C D F) ( map-functor-Precategory C D G) is-set-natural-transformation-Precategory : is-set (natural-transformation-Precategory C D F G) is-set-natural-transformation-Precategory = is-set-natural-transformation-map-Precategory C D ( map-functor-Precategory C D F) ( map-functor-Precategory C D G) natural-transformation-set-Precategory : Set (l1 ⊔ l2 ⊔ l4) pr1 (natural-transformation-set-Precategory) = natural-transformation-Precategory C D F G pr2 (natural-transformation-set-Precategory) = is-set-natural-transformation-Precategory extensionality-natural-transformation-Precategory : (α β : natural-transformation-Precategory C D F G) → ( α = β) ≃ ( hom-family-natural-transformation-Precategory C D F G α ~ hom-family-natural-transformation-Precategory C D F G β) extensionality-natural-transformation-Precategory = extensionality-natural-transformation-map-Precategory C D ( map-functor-Precategory C D F) ( map-functor-Precategory C D G) eq-htpy-hom-family-natural-transformation-Precategory : (α β : natural-transformation-Precategory C D F G) → ( hom-family-natural-transformation-Precategory C D F G α ~ hom-family-natural-transformation-Precategory C D F G β) → α = β eq-htpy-hom-family-natural-transformation-Precategory = eq-htpy-hom-family-natural-transformation-map-Precategory C D ( map-functor-Precategory C D F) ( map-functor-Precategory C D G)
Categorical laws for natural transformations
module _ {l1 l2 l3 l4 : Level} (C : Precategory l1 l2) (D : Precategory l3 l4) where right-unit-law-comp-natural-transformation-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-natural-transformation-Precategory F G = right-unit-law-comp-natural-transformation-map-Precategory C D ( map-functor-Precategory C D F) ( map-functor-Precategory C D G) left-unit-law-comp-natural-transformation-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-natural-transformation-Precategory F G = left-unit-law-comp-natural-transformation-map-Precategory C D ( map-functor-Precategory C D F) ( map-functor-Precategory C D G) associative-comp-natural-transformation-Precategory : (F G H I : functor-Precategory C D) (α : natural-transformation-Precategory C D F G) (β : natural-transformation-Precategory C D G H) (γ : natural-transformation-Precategory C D H I) → comp-natural-transformation-Precategory C D F G I ( comp-natural-transformation-Precategory C D G H I γ β) α = comp-natural-transformation-Precategory C D F H I γ ( comp-natural-transformation-Precategory C D F G H β α) associative-comp-natural-transformation-Precategory F G H I = associative-comp-natural-transformation-map-Precategory C D ( map-functor-Precategory C D F) ( map-functor-Precategory C D G) ( map-functor-Precategory C D H) ( map-functor-Precategory C D I) inv-associative-comp-natural-transformation-Precategory : (F G H I : functor-Precategory C D) (α : natural-transformation-Precategory C D F G) (β : natural-transformation-Precategory C D G H) (γ : natural-transformation-Precategory C D H I) → comp-natural-transformation-Precategory C D F H I γ ( comp-natural-transformation-Precategory C D F G H β α) = comp-natural-transformation-Precategory C D F G I ( comp-natural-transformation-Precategory C D G H I γ β) α inv-associative-comp-natural-transformation-Precategory F G H I = inv-associative-comp-natural-transformation-map-Precategory C D ( map-functor-Precategory C D F) ( map-functor-Precategory C D G) ( map-functor-Precategory C D H) ( map-functor-Precategory C D I)
Recent changes
- 2023-11-27. Fredrik Bakke. Refactor categories to carry a bidirectional witness of associativity (#945).
- 2023-11-01. Fredrik Bakke. Opposite categories, gaunt categories, replete subprecategories, large Yoneda, and miscellaneous additions (#880).
- 2023-09-27. Fredrik Bakke. Presheaf categories (#801).