:PROPERTIES: :ID: fc2f7c1f-079c-4bd1-80d4-9905ba1b366c :mtime: 20230927112112 20230918150937 20230807124111 :ctime: 20230807113442 :END: #+title: Natural Transformation #+filetags: :public:project:category:theory: * Definition A Natural Transformation is a morphism between Functors. Let $C , C'$ be categories. Let $F_{1} \quad F_{2} : C \to C'$ be functors from $C$ to $C'$. We say that $\tau : F_{1} \to F_{2}$ is a natural transformation from $F_1$ to $F_{2}$ if $\tau$ is a function which assigns to every object $c \in C$ an arrow $\tau(c) : F_1(c) \to F_2(c)$ such that for all arrows $f : c \to c'$ in $C$ we have that $F_1(f) \gg \tau(c') = \tau(c) \gg F_2(f)$ In Agda, we would write a natural transformation as #+NAME: natural transformation in agda #+BEGIN_SRC agda record NaturalTransformation {obj₁ : Set o₁} {obj₂ : Set o₂} {_⇨₁_ : obj₁ → obj₁ → Set ℓ₁} {_⇨₂_ : obj₂ → obj₂ → Set ℓ₂} {C : Category _⇨₁_} {D : Category _⇨₂_} (F₁ : Functor C D) (F₂ : Functor C D) : Set (o₁ ⊔ o₂ ⊔ ℓ₁ ⊔ ℓ₂) where field τ : (c : obj₁) → (Fₒ F₁ c ⇨₂ Fₒ F₂ c) τ-natural : {c c' : obj₁} {f : c ⇨₁ c'} → (_≫_ D (τ c) (Fₐ F₂ f)) ≡ (_≫_ D (Fₐ F₁ f) (τ c')) #+END_SRC