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 1.6.1: Product Categories *)
9 (******************************************************************************)
11 Section ProductCategories.
13 Context `(C1:Category Ob1 Hom1).
14 Context `(C2:Category Ob2 Hom2).
16 (* trying to use the standard "prod" here causes a universe inconsistency once we get to coqBinoidal;
17 * moreover, using a general fully-polymorphic pair type seems to trigger some serious memory leaks
19 Inductive prod_obj : Type := pair_obj : C1 -> C2 -> prod_obj.
20 Definition fst_obj x := match x with pair_obj a _ => a end.
21 Definition snd_obj x := match x with pair_obj _ b => b end.
23 Inductive prod_mor (a b:prod_obj) : Type :=
25 ((fst_obj a)~~{C1}~~>(fst_obj b)) ->
26 ((snd_obj a)~~{C2}~~>(snd_obj b)) ->
28 Definition fst_mor {a b:prod_obj}(x:prod_mor a b) := match x with pair_mor a _ => a end.
29 Definition snd_mor {a b:prod_obj}(x:prod_mor a b) := match x with pair_mor _ b => b end.
31 Definition ProductCategory : Category prod_obj prod_mor.
33 {| id := fun (a:prod_obj) => pair_mor a a (id (fst_obj a)) (id (snd_obj a))
34 ; comp := fun a b c (f:prod_mor a b) (g:prod_mor b c) =>
35 match f with pair_mor f1 f2 => match g with pair_mor g1 g2 => pair_mor _ _ (f1>>>g1) (f2>>>g2) end end
36 ; eqv := fun a b (f:prod_mor a b) (g:prod_mor a b) =>
37 match f with pair_mor f1 f2 => match g with pair_mor g1 g2 => (f1~~g1)/\(f2~~g2) end end
40 abstract (apply Build_Equivalence; intros; simpl; intros;
41 [ unfold Reflexive; intros; case x; intros; split; reflexivity
42 | unfold Symmetric; intros; destruct y; destruct x; split; case H; intros; symmetry; auto
43 | unfold Transitive; intros; destruct x; destruct z; destruct y; split; case H; case H0; intros; auto ]).
44 abstract (intros; unfold Proper; simpl; unfold respectful; intros;
45 destruct x0; destruct y0; destruct x; destruct y;
46 case H; intros; case H0; intros; split; auto).
47 abstract (intros; destruct a; destruct b; case f; intros; simpl; setoid_rewrite left_identity; split; reflexivity).
48 abstract (intros; destruct a; destruct b; case f; intros; simpl; setoid_rewrite right_identity; split; symmetry; reflexivity).
49 abstract (intros; destruct a; destruct b; destruct c; case f; intros; destruct d; simpl; case g; intros;
50 destruct h; setoid_rewrite associativity; split; reflexivity).
52 End ProductCategories.
54 Implicit Arguments pair_obj [ Ob1 Hom1 Ob2 Hom2 C1 C2 ].
55 Implicit Arguments pair_mor [ Ob1 Hom1 Ob2 Hom2 C1 C2 ].
56 Notation "C ×× D" := (ProductCategory C D).
58 Section ProductCategoryFunctors.
60 Context `{C:Category}.
61 Context `{D:Category}.
63 Definition func_pi1 : Functor (C ×× D) C (fun c => fst_obj _ _ c).
64 refine {| fmor := fun a b (f:prod_mor _ _ a b) => fst_mor _ _ f |}; intros; simpl in *.
65 destruct f; destruct f'; simpl in *; destruct H; auto.
67 destruct f; destruct g; simpl in *; auto.
70 Definition func_pi2 : Functor (C ×× D) D (fun c => snd_obj _ _ c).
71 refine {| fmor := fun a b (f:prod_mor _ _ a b) => snd_mor _ _ f |}; intros; simpl in *.
72 destruct f; destruct f'; simpl in *; destruct H; auto.
74 destruct f; destruct g; simpl in *; auto.
77 Definition llecnac_fmor (I:C) : forall (a b:D)(f:a~~{D}~~>b), (pair_obj I a)~~{C××D}~~>(pair_obj I b).
78 intros; apply pair_mor; [ exact (id I) | auto ].
80 Definition func_llecnac (I:C) : Functor D (C ×× D) (pair_obj I).
81 refine {| fmor := fun a b f => llecnac_fmor I a b f |}.
82 abstract (intros; simpl; repeat split; simpl; auto).
83 abstract (intros; simpl; repeat split; simpl; auto).
84 abstract (intros; simpl; repeat split; simpl; auto).
87 Definition rlecnac_fmor (I:D) : forall (a b:C)(f:a~~{C}~~>b), (pair_obj a I)~~{C××D}~~>(pair_obj b I).
88 intros; apply pair_mor; [ auto | exact (id I) ].
90 Definition func_rlecnac (I:D) : Functor C (C ×× D) (fun c => (pair_obj c I)).
91 refine {| fmor := fun a b f => rlecnac_fmor I a b f |}.
92 abstract (intros; simpl; repeat split; simpl; auto).
93 abstract (intros; simpl; repeat split; simpl; auto).
94 abstract (intros; simpl; repeat split; simpl; auto).
97 Context `{E:Category}.
98 Definition cossa : ((C ×× D) ×× E) -> (C ×× (D ×× E)).
100 case X as [a1 a2]; intros.
101 case a1 as [a11 a12]; intros.
102 exact (pair_obj a11 (pair_obj a12 a2)).
104 Definition cossa_fmor (a:((C ×× D) ×× E)) (b:((C ×× D) ×× E)) (f:a~~{(C ×× D) ×× E}~~>b) : (cossa a)~~{C ×× (D ×× E)}~~>(cossa b).
105 case a as [ [a11 a12] a2];
106 case b as [ [b11 b12] b2];
107 case f as [ [f11 f12] f2];
108 apply pair_mor; auto;
109 apply pair_mor; auto.
111 Definition func_cossa : Functor ((C ×× D) ×× E) (C ×× (D ×× E)) cossa.
112 refine {| fmor := fun a b f => cossa_fmor a b f |}.
114 case a as [ [a11 a12] a2];
115 case b as [ [b11 b12] b2];
116 case f as [ [f11 f12] f2];
117 case f' as [ [g11 g12] g2];
118 case H; intro H'; case H';
119 split; [ idtac | split ]; auto).
120 abstract (intros; case a as [ [a11 a12] a2]; split; [ idtac | split ]; reflexivity).
122 case a as [ [a11 a12] a2];
123 case b as [ [b11 b12] b2];
124 case c as [ [c11 c12] c2];
125 case f as [ [f11 f12] f2];
126 case g as [ [g11 g12] g2];
127 intros; reflexivity).
129 End ProductCategoryFunctors.
132 Context `{C1:Category}`{C2:Category}`{C3:Category}`{C4:Category}{Fobj1}{Fobj2}(F1:Functor C1 C2 Fobj1)(F2:Functor C3 C4 Fobj2).
134 Definition functor_product_fobj a := pair_obj (Fobj1 (fst_obj _ _ a)) (Fobj2 (snd_obj _ _ a)).
136 Definition functor_product_fmor (a b:(C1 ×× C3))(f:a~~{C1 ×× C3}~~>b)
137 : (functor_product_fobj a)~~{C2 ×× C4}~~>(functor_product_fobj b).
140 apply pair_mor; simpl;
141 [ apply (fmor F1) | apply (fmor F2) ];
147 Definition func_prod : Functor (C1 ×× C3) (C2 ×× C4) functor_product_fobj.
148 refine {| fmor := fun a b (f:a~~{C1 ×× C3}~~>b) => functor_product_fmor a b f |}.
149 abstract (intros; destruct a; try destruct b; destruct f; destruct f'; split; destruct H;
150 [ apply (@fmor_respects _ _ _ _ _ _ _ F1 _ _ h h1)
151 | apply (@fmor_respects _ _ _ _ _ _ _ F2 _ _ h0 h2)
153 abstract (intros; case a; intros; simpl; split; apply fmor_preserves_id).
154 abstract (intros; destruct a; destruct b; destruct c; case f; intros; case g; intros; split; simpl; apply fmor_preserves_comp).
158 Notation "f **** g" := (func_prod f g).
160 Instance iso_prod `{C:Category}`{D:Category}{a b:C}{c d:D}(ic:a≅b)(id:@Isomorphic _ _ D c d)
161 : @Isomorphic _ _ (C ×× D) (pair_obj a c) (pair_obj b d) :=
162 { iso_forward := pair_mor (pair_obj a c) (pair_obj b d) (iso_forward ic) (iso_forward id)
163 ; iso_backward := pair_mor (pair_obj b d) (pair_obj a c) (iso_backward ic) (iso_backward id)
165 abstract (simpl; split; apply iso_comp1).
166 abstract (simpl; split; apply iso_comp2).