src/ProductCategories_ch1_6_1.v

   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.
   6
   7 (******************************************************************************)
   8 (* Chapter 1.6.1: Product Categories                                          *)
   9 (******************************************************************************)
  10
  11 Section ProductCategories.
  12
  13   Context `(C1:Category Ob1 Hom1).
  14   Context `(C2:Category Ob2 Hom2).
  15
  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
  18    * in Coq *)
  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.
  22
  23   Inductive  prod_mor (a b:prod_obj) : Type :=
  24     pair_mor :
  25       ((fst_obj a)~~{C1}~~>(fst_obj b)) ->
  26       ((snd_obj a)~~{C2}~~>(snd_obj b)) ->
  27       prod_mor a 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.
  30
  31   Definition ProductCategory : Category prod_obj prod_mor.
  32     refine
  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
  38     |}.
  39     intros.
  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).
  51       Defined.
  52 End ProductCategories.
  53
  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).
  57
  58 Section ProductCategoryFunctors.
  59
  60   Context `{C:Category}.
  61   Context `{D:Category}.
  62
  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.
  66     reflexivity.
  67     destruct f; destruct g; simpl in *; auto.
  68     Defined.
  69
  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.
  73     reflexivity.
  74     destruct f; destruct g; simpl in *; auto.
  75     Defined.
  76
  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 ].
  79     Defined.
  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).
  85     Defined.
  86
  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) ].
  89     Defined.
  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).
  95     Defined.
  96
  97   Context `{E:Category}.
  98   Definition cossa : ((C ×× D) ×× E) -> (C ×× (D ×× E)).
  99     intros.
 100     case X as [a1 a2]; intros.
 101     case a1 as [a11 a12]; intros.
 102     exact (pair_obj a11 (pair_obj a12 a2)).
 103     Defined.
 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.
 110     Defined.
 111   Definition func_cossa : Functor ((C ×× D) ×× E) (C ×× (D ×× E)) cossa.
 112     refine {| fmor := fun a b f => cossa_fmor a b f |}.
 113     abstract (intros;
 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).
 121     abstract (intros;
 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).
 128     Defined.
 129 End ProductCategoryFunctors.
 130
 131 Section func_prod.
 132   Context `{C1:Category}`{C2:Category}`{C3:Category}`{C4:Category}{Fobj1}{Fobj2}(F1:Functor C1 C2 Fobj1)(F2:Functor C3 C4 Fobj2).
 133
 134   Definition functor_product_fobj a := pair_obj (Fobj1 (fst_obj _ _ a)) (Fobj2 (snd_obj _ _ a)).
 135
 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).
 138   destruct a; intros.
 139   destruct b; intros.
 140   apply pair_mor; simpl;
 141   [ apply (fmor F1) | apply (fmor F2) ];
 142   case f; intros;
 143   auto.
 144   Defined.
 145
 146   Hint Unfold fst_obj.
 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)
 152               ]; auto).
 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).
 155     Defined.
 156
 157 End func_prod.
 158 Notation "f **** g" := (func_prod f g).
 159
 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)
 164   }.
 165   abstract (simpl; split; apply iso_comp1).
 166   abstract (simpl; split; apply iso_comp2).
 167   Defined.
 168
 169
 170