1 Generalizable All Variables.
2 Require Import Preamble.
3 Require Import Categories_ch1_3.
4 Require Import Functors_ch1_4.
5 Require Import Isomorphisms_ch1_5.
7 (*******************************************************************************)
8 (* Chapter 7.4: Natural Transformations *)
9 (*******************************************************************************)
12 Structure NaturalTransformation `{C1:Category}`{C2:Category}{Fobj1 Fobj2:C1->C2}(F1:Functor C1 C2 Fobj1)(F2:Functor C1 C2 Fobj2) :=
13 { nt_component : forall c:C1, (Fobj1 c) ~~{C2}~~> (Fobj2 c)
14 ; nt_commutes : forall `(f:A~>B), (nt_component A) >>> F2 \ f ~~ F1 \ f >>> (nt_component B)
16 Notation "F ~~~> G" := (@NaturalTransformation _ _ _ _ _ _ _ _ F G) : category_scope.
17 Coercion nt_component : NaturalTransformation >-> Funclass.
19 (* the identity natural transformation *)
20 Definition nt_id `{C:Category}`{D:Category}{Fobj}(F:Functor C D Fobj) : NaturalTransformation F F.
21 apply (@Build_NaturalTransformation _ _ _ _ _ _ _ _ F F (fun c => id (F c))).
23 setoid_rewrite left_identity;
24 setoid_rewrite right_identity;
27 Definition nt_comp `{C:Category}`{D:Category}
28 {Fobj}{F:Functor C D Fobj}
29 {Gobj}{G:Functor C D Gobj}
30 {Hobj}{H:Functor C D Hobj}
31 (nt_f_g:F ~~~> G) (nt_g_h:G ~~~> H) : F ~~~> H.
32 apply (@Build_NaturalTransformation _ _ _ _ _ _ _ _ F H (fun c => nt_f_g c >>> nt_g_h c)).
34 set (@nt_commutes _ _ C _ _ D _ _ F G nt_f_g) as comm1;
35 set (@nt_commutes _ _ C _ _ D _ _ G H nt_g_h) as comm2;
36 setoid_rewrite associativity;
38 setoid_rewrite <- associativity;
39 setoid_rewrite <- comm1;