# Library Exercise_4_3_1_3

Require Import Utf8.
Require Import NaturalTransformation.
Require Import Common.

Set Implicit Arguments.

Generalizable All Variables.

# Exercise 4.3.1.3

Section Exercise_4_3_1_3.

## Problem

Let F : C D be a functor. Suppose someone said "the identity on F is a natural transformation from F to itself." What might they mean? If it is somehow true, what are the components of this natural transformation?

Context `(C : @Category objC).
Context `(D : @Category objD).
Variable F : Functor C D.

Definition IdentityNaturalTransformation' : NaturalTransformation F F.
refine {| ComponentsOf := (fun c Identity (F c)) |}.
abstract (simpl; intros; rewrite LeftIdentity, RightIdentity; reflexivity).
Defined.

Lemma LeftIdentityNaturalTransformation'
: (F' : Functor C D)
(T : NaturalTransformation F' F),
NTComposeT IdentityNaturalTransformation' T = T.
Proof.
intros; apply NaturalTransformation_Eq; simpl; auto with morphism.
Qed.

Lemma RightIdentityNaturalTransformation'
: (F' : Functor C D)
(T : NaturalTransformation F F'),
NTComposeT T IdentityNaturalTransformation' = T.
Proof.
intros; apply NaturalTransformation_Eq; simpl; auto with morphism.
Qed.
End Exercise_4_3_1_3.