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.