Natural transformations between maps between precategories
Content created by Fredrik Bakke and Egbert Rijke.
Created on 2023-09-26.
Last modified on 2024-03-11.
module category-theory.natural-transformations-maps-precategories where
Imports
open import category-theory.commuting-squares-of-morphisms-in-precategories open import category-theory.maps-precategories open import category-theory.precategories open import foundation.action-on-identifications-functions open import foundation.dependent-pair-types open import foundation.embeddings open import foundation.equivalences open import foundation.function-extensionality open import foundation.function-types open import foundation.homotopies open import foundation.identity-types open import foundation.propositions open import foundation.sets open import foundation.strictly-involutive-identity-types open import foundation.subtypes open import foundation.universe-levels
Idea
Given precategories C and D, a natural
transformation from a
map of precategories 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 : map-Precategory C D) where hom-family-map-Precategory : UU (l1 ⊔ l4) hom-family-map-Precategory = (x : obj-Precategory C) → hom-Precategory D ( obj-map-Precategory C D F x) ( obj-map-Precategory C D G x) naturality-hom-family-map-Precategory : hom-family-map-Precategory → {x y : obj-Precategory C} (f : hom-Precategory C x y) → UU l4 naturality-hom-family-map-Precategory γ {x} {y} f = coherence-square-hom-Precategory D ( hom-map-Precategory C D F f) ( γ x) ( γ y) ( hom-map-Precategory C D G f) is-natural-transformation-map-Precategory : hom-family-map-Precategory → UU (l1 ⊔ l2 ⊔ l4) is-natural-transformation-map-Precategory γ = {x y : obj-Precategory C} (f : hom-Precategory C x y) → naturality-hom-family-map-Precategory γ f natural-transformation-map-Precategory : UU (l1 ⊔ l2 ⊔ l4) natural-transformation-map-Precategory = Σ ( hom-family-map-Precategory) ( is-natural-transformation-map-Precategory) hom-family-natural-transformation-map-Precategory : natural-transformation-map-Precategory → hom-family-map-Precategory hom-family-natural-transformation-map-Precategory = pr1 naturality-natural-transformation-map-Precategory : (γ : natural-transformation-map-Precategory) → is-natural-transformation-map-Precategory ( hom-family-natural-transformation-map-Precategory γ) naturality-natural-transformation-map-Precategory = pr2
Composition and identity of natural transformations
module _ {l1 l2 l3 l4 : Level} (C : Precategory l1 l2) (D : Precategory l3 l4) where id-natural-transformation-map-Precategory : (F : map-Precategory C D) → natural-transformation-map-Precategory C D F F pr1 (id-natural-transformation-map-Precategory F) x = id-hom-Precategory D pr2 (id-natural-transformation-map-Precategory F) f = ( right-unit-law-comp-hom-Precategory D ( hom-map-Precategory C D F f)) ∙ ( inv ( left-unit-law-comp-hom-Precategory D ( hom-map-Precategory C D F f))) comp-natural-transformation-map-Precategory : (F G H : map-Precategory C D) → natural-transformation-map-Precategory C D G H → natural-transformation-map-Precategory C D F G → natural-transformation-map-Precategory C D F H pr1 (comp-natural-transformation-map-Precategory F G H β α) x = comp-hom-Precategory D ( hom-family-natural-transformation-map-Precategory C D G H β x) ( hom-family-natural-transformation-map-Precategory C D F G α x) pr2 (comp-natural-transformation-map-Precategory F G H β α) {X} {Y} f = ( inv ( associative-comp-hom-Precategory D ( hom-map-Precategory C D H f) ( hom-family-natural-transformation-map-Precategory C D G H β X) ( hom-family-natural-transformation-map-Precategory C D F G α X))) ∙ ( ap ( comp-hom-Precategory' D ( hom-family-natural-transformation-map-Precategory C D F G α X)) ( naturality-natural-transformation-map-Precategory C D G H β f)) ∙ ( associative-comp-hom-Precategory D ( hom-family-natural-transformation-map-Precategory C D G H β Y) ( hom-map-Precategory C D G f) ( hom-family-natural-transformation-map-Precategory C D F G α X)) ∙ ( ap ( comp-hom-Precategory D ( hom-family-natural-transformation-map-Precategory C D G H β Y)) ( naturality-natural-transformation-map-Precategory C D F G α f)) ∙ ( inv ( associative-comp-hom-Precategory D ( hom-family-natural-transformation-map-Precategory C D G H β Y) ( hom-family-natural-transformation-map-Precategory C D F G α Y) ( hom-map-Precategory C D F f)))
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 : map-Precategory C D) where is-prop-is-natural-transformation-map-Precategory : ( γ : hom-family-map-Precategory C D F G) → is-prop (is-natural-transformation-map-Precategory C D F G γ) is-prop-is-natural-transformation-map-Precategory γ = is-prop-implicit-Π ( λ x → is-prop-implicit-Π ( λ y → is-prop-Π ( λ f → is-set-hom-Precategory D ( obj-map-Precategory C D F x) ( obj-map-Precategory C D G y) ( comp-hom-Precategory D ( hom-map-Precategory C D G f) ( γ x)) ( comp-hom-Precategory D ( γ y) ( hom-map-Precategory C D F f))))) is-natural-transformation-prop-map-Precategory : ( γ : hom-family-map-Precategory C D F G) → Prop (l1 ⊔ l2 ⊔ l4) pr1 (is-natural-transformation-prop-map-Precategory α) = is-natural-transformation-map-Precategory C D F G α pr2 (is-natural-transformation-prop-map-Precategory α) = is-prop-is-natural-transformation-map-Precategory α
The set of natural transformations
module _ {l1 l2 l3 l4 : Level} (C : Precategory l1 l2) (D : Precategory l3 l4) (F G : map-Precategory C D) where is-emb-hom-family-natural-transformation-map-Precategory : is-emb (hom-family-natural-transformation-map-Precategory C D F G) is-emb-hom-family-natural-transformation-map-Precategory = is-emb-inclusion-subtype ( is-natural-transformation-prop-map-Precategory C D F G) emb-hom-family-natural-transformation-map-Precategory : natural-transformation-map-Precategory C D F G ↪ hom-family-map-Precategory C D F G emb-hom-family-natural-transformation-map-Precategory = emb-subtype (is-natural-transformation-prop-map-Precategory C D F G) is-set-natural-transformation-map-Precategory : is-set (natural-transformation-map-Precategory C D F G) is-set-natural-transformation-map-Precategory = is-set-Σ ( is-set-Π ( λ x → is-set-hom-Precategory D ( obj-map-Precategory C D F x) ( obj-map-Precategory C D G x))) ( λ α → is-set-type-Set ( set-Prop ( is-natural-transformation-prop-map-Precategory C D F G α))) natural-transformation-map-set-Precategory : Set (l1 ⊔ l2 ⊔ l4) pr1 (natural-transformation-map-set-Precategory) = natural-transformation-map-Precategory C D F G pr2 (natural-transformation-map-set-Precategory) = is-set-natural-transformation-map-Precategory extensionality-natural-transformation-map-Precategory : (α β : natural-transformation-map-Precategory C D F G) → ( α ＝ β) ≃ ( hom-family-natural-transformation-map-Precategory C D F G α ~ hom-family-natural-transformation-map-Precategory C D F G β) extensionality-natural-transformation-map-Precategory α β = ( equiv-funext) ∘e ( equiv-ap-emb emb-hom-family-natural-transformation-map-Precategory) eq-htpy-hom-family-natural-transformation-map-Precategory : (α β : natural-transformation-map-Precategory C D F G) → ( hom-family-natural-transformation-map-Precategory C D F G α ~ hom-family-natural-transformation-map-Precategory C D F G β) → α ＝ β eq-htpy-hom-family-natural-transformation-map-Precategory α β = map-inv-equiv (extensionality-natural-transformation-map-Precategory α β)
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-map-Precategory : (F G : map-Precategory C D) (α : natural-transformation-map-Precategory C D F G) → comp-natural-transformation-map-Precategory C D F F G α ( id-natural-transformation-map-Precategory C D F) ＝ α right-unit-law-comp-natural-transformation-map-Precategory F G α = eq-htpy-hom-family-natural-transformation-map-Precategory C D F G ( comp-natural-transformation-map-Precategory C D F F G α ( id-natural-transformation-map-Precategory C D F)) ( α) ( right-unit-law-comp-hom-Precategory D ∘ hom-family-natural-transformation-map-Precategory C D F G α) left-unit-law-comp-natural-transformation-map-Precategory : (F G : map-Precategory C D) (α : natural-transformation-map-Precategory C D F G) → comp-natural-transformation-map-Precategory C D F G G ( id-natural-transformation-map-Precategory C D G) α ＝ α left-unit-law-comp-natural-transformation-map-Precategory F G α = eq-htpy-hom-family-natural-transformation-map-Precategory C D F G ( comp-natural-transformation-map-Precategory C D F G G ( id-natural-transformation-map-Precategory C D G) α) ( α) ( left-unit-law-comp-hom-Precategory D ∘ hom-family-natural-transformation-map-Precategory C D F G α) associative-comp-natural-transformation-map-Precategory : (F G H I : map-Precategory C D) (α : natural-transformation-map-Precategory C D F G) (β : natural-transformation-map-Precategory C D G H) (γ : natural-transformation-map-Precategory C D H I) → comp-natural-transformation-map-Precategory C D F G I ( comp-natural-transformation-map-Precategory C D G H I γ β) α ＝ comp-natural-transformation-map-Precategory C D F H I γ ( comp-natural-transformation-map-Precategory C D F G H β α) associative-comp-natural-transformation-map-Precategory F G H I α β γ = eq-htpy-hom-family-natural-transformation-map-Precategory C D F I _ _ ( λ x → associative-comp-hom-Precategory D ( hom-family-natural-transformation-map-Precategory C D H I γ x) ( hom-family-natural-transformation-map-Precategory C D G H β x) ( hom-family-natural-transformation-map-Precategory C D F G α x)) involutive-eq-associative-comp-natural-transformation-map-Precategory : (F G H I : map-Precategory C D) (α : natural-transformation-map-Precategory C D F G) (β : natural-transformation-map-Precategory C D G H) (γ : natural-transformation-map-Precategory C D H I) → comp-natural-transformation-map-Precategory C D F G I ( comp-natural-transformation-map-Precategory C D G H I γ β) α ＝ⁱ comp-natural-transformation-map-Precategory C D F H I γ ( comp-natural-transformation-map-Precategory C D F G H β α) involutive-eq-associative-comp-natural-transformation-map-Precategory F G H I α β γ = involutive-eq-eq ( associative-comp-natural-transformation-map-Precategory F G H I α β γ)
Recent changes
- 2024-03-11. Fredrik Bakke. Refactor category theory to use strictly involutive identity types (#1052).
- 2024-01-11. Fredrik Bakke. Rename
is-prop-Π'tois-prop-implicit-ΠandΠ-Prop'toimplicit-Π-Prop(#997). - 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-26. Fredrik Bakke and Egbert Rijke. Maps of categories, functor categories, and small subprecategories (#794).