1 Generalizable All Variables.
2 Require Import Notations.
3 Require Import Categories_ch1_3.
4 Require Import Functors_ch1_4.
5 Require Import Isomorphisms_ch1_5.
6 Require Import NaturalTransformations_ch7_4.
7 Require Import NaturalIsomorphisms_ch7_5.
9 (*******************************************************************************)
10 (* Chapter 7.5 and 7.7: Functor Categories *)
11 (*******************************************************************************)
14 Instance FunctorCategory `(C:Category)`(D:Category)
15 : Category { Fobj : C->D & Functor C D Fobj } (fun F G => (projT2 F) ~~~> (projT2 G)) :=
16 { id := fun F => nt_id (projT2 F)
17 ; comp := fun F G H nt_f_g nt_g_h => nt_comp nt_f_g nt_g_h
18 ; eqv := fun F G nt1 nt2 => forall c, (nt1 c) ~~ (nt2 c)
21 (apply Build_Equivalence;
22 [ unfold Reflexive; unfold respectful; simpl; intros; reflexivity
23 | unfold Symmetric; unfold respectful; simpl; intros; symmetry; auto
24 | unfold Transitive; unfold respectful; simpl; intros; etransitivity; [ apply H | auto ] ]).
25 abstract (intros; unfold Proper; unfold respectful; simpl; intros; setoid_rewrite H0; setoid_rewrite H; reflexivity).
26 abstract (intros; simpl; apply left_identity).
27 abstract (intros; simpl; apply right_identity).
28 abstract (intros; simpl; apply associativity).
31 (* functors compose with each other, natural transformations compose with each other -- but you can also
32 * compose a functor with a natural transformation! *)
33 Definition LeftWhisker
34 `{C:Category}`{D:Category}`{E:Category}
35 {Fobj}{F:Functor C D Fobj}
36 {Gobj}{G:Functor C D Gobj}
38 {Hobj}(H:Functor D E Hobj) : ((F >>>> H) ~~~> (G >>>> H)).
39 apply Build_NaturalTransformation with (nt_component:=(fun c => H \ (nat c))).
42 set (@nt_commutes _ _ _ _ _ _ F _ _ G nat) as nat';
43 setoid_rewrite fmor_preserves_comp;
44 setoid_rewrite <- nat';
45 setoid_rewrite <- (fmor_preserves_comp H);
49 Definition RightWhisker
50 `{C:Category}`{D:Category}`{E:Category}
51 {Fobj}(F:Functor C D Fobj)
52 {Gobj}{G:Functor D E Gobj}
53 {Hobj}{H:Functor D E Hobj} : (G ~~~> H) -> ((F >>>> G) ~~~> (F >>>> H)).
55 apply Build_NaturalTransformation with (nt_component:=(fun c => (nat (F c)))).
58 set (@nt_commutes _ _ _ _ _ _ G _ _ H nat) as nat';
63 (* also sometimes called "horizontal composition" *)
64 Definition GodementMultiplication
65 `{A:Category}`{B:Category}`{C:Category}
66 {F0obj}{F0:Functor A B F0obj}
67 {F1obj}{F1:Functor A B F1obj}
68 {G0obj}{G0:Functor B C G0obj}
69 {G1obj}{G1:Functor B C G1obj}
70 : (F0~~~>F1) -> (G0~~~>G1) -> ((F0 >>>> G0)~~~>(F1 >>>> G1)).
73 apply Build_NaturalTransformation with (nt_component:=(fun (a:A) => G0 \ (phi a) >>> psi (F1 a))).
75 set (@nt_commutes _ _ _ _ _ _ F0 _ _ F1 phi) as comm1;
76 set (@nt_commutes _ _ _ _ _ _ G0 _ _ G1 psi) as comm2;
77 setoid_rewrite <- comm2;
79 setoid_rewrite associativity;
80 setoid_rewrite fmor_preserves_comp;
82 setoid_rewrite <- fmor_preserves_comp;
83 repeat setoid_rewrite <- associativity;
84 apply comp_respects; try reflexivity;
88 (* this operation is also a bifunctor from (FunctorCategory A B)*(FunctorCategory B C) to (FunctorCategory A C);