src/PreMonoidalCategories.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 Require Import EpicMonic_ch2_1.
   7 Require Import InitialTerminal_ch2_2.
   8 Require Import Subcategories_ch7_1.
   9 Require Import NaturalTransformations_ch7_4.
  10 Require Import NaturalIsomorphisms_ch7_5.
  11 Require Import Coherence_ch7_8.
  12 Require Import BinoidalCategories.
  13
  14 (* not in Awodey *)
  15 Class PreMonoidalCat `(bc:BinoidalCat(C:=C))(I:C) :=
  16 { pmon_I               := I
  17 ; pmon_bin             := bc
  18 ; pmon_cat             := C
  19 ; pmon_assoc           : forall a b, (bin_second a >>>> bin_first b) <~~~> (bin_first b >>>> bin_second a)
  20 ; pmon_cancelr         :                               (bin_first I) <~~~> functor_id C
  21 ; pmon_cancell         :                              (bin_second I) <~~~> functor_id C
  22 ; pmon_pentagon        : Pentagon (fun a b c f => f ⋉ c) (fun a b c f => c ⋊ f) (fun a b c => #((pmon_assoc a c) b))
  23 ; pmon_triangle        : Triangle (fun a b c f => f ⋉ c) (fun a b c f => c ⋊ f) (fun a b c => #((pmon_assoc a c) b))
  24                                   (fun a => #(pmon_cancell a)) (fun a => #(pmon_cancelr a))
  25 ; pmon_assoc_rr        :  forall a b, (bin_first  (a⊗b)) <~~~> (bin_first  a >>>> bin_first  b)
  26 ; pmon_assoc_ll        :  forall a b, (bin_second (a⊗b)) <~~~> (bin_second b >>>> bin_second a)
  27 ; pmon_coherent_r      :  forall a c d:C,  #(pmon_assoc_rr c d a) ~~ #(pmon_assoc a d c)⁻¹
  28 ; pmon_coherent_l      :  forall a c d:C,  #(pmon_assoc_ll c a d) ~~ #(pmon_assoc c d a)
  29 ; pmon_assoc_central   :  forall a b c, CentralMorphism #(pmon_assoc   a b c)
  30 ; pmon_cancelr_central :  forall a    , CentralMorphism #(pmon_cancelr a)
  31 ; pmon_cancell_central :  forall a    , CentralMorphism #(pmon_cancell a)
  32 }.
  33 (*
  34  * Premonoidal categories actually have three associators (the "f"
  35  * indicates the position in which the operation is natural:
  36  *
  37  *  assoc    : (A ⋊ f) ⋉ C <->  A ⋊ (f ⋉  C)
  38  *  assoc_rr : (f ⋉ B) ⋉ C <->  f ⋉ (B  ⊗ C)
  39  *  assoc_ll : (A ⋊ B) ⋊ f <-> (A ⊗  B) ⋊ f
  40  *
  41  * Fortunately, in a monoidal category these are all the same natural
  42  * isomorphism (and in any case -- monoidal or not -- the objects in
  43  * the left column are all the same and the objects in the right
  44  * column are all the same).  This formalization assumes that is the
  45  * case even for premonoidal categories with non-central maps, in
  46  * order to keep the complexity manageable.  I don't know much about
  47  * the consequences of having them and letting them be different; you
  48  * might need extra versions of the triangle/pentagon diagrams.
  49  *)
  50
  51 Implicit Arguments pmon_cancell [ Ob Hom C bin_obj' bc I PreMonoidalCat ].
  52 Implicit Arguments pmon_cancelr [ Ob Hom C bin_obj' bc I PreMonoidalCat ].
  53 Implicit Arguments pmon_assoc   [ Ob Hom C bin_obj' bc I PreMonoidalCat ].
  54 Coercion pmon_bin : PreMonoidalCat >-> BinoidalCat.
  55
  56 (* this turns out to be Exercise VII.1.1 from Mac Lane's CWM *)
  57 Lemma MacLane_ex_VII_1_1 `{mn:PreMonoidalCat(I:=EI)} b a
  58   :
  59   let    α := fun a b c => #((pmon_assoc a c) b)
  60   in     α a b EI >>> _ ⋊ #(pmon_cancelr _) ~~ #(pmon_cancelr _).
  61
  62   intros.  simpl in α.
  63
  64   (* following Mac Lane's hint, we aim for (λ >>> α >>> λ×1)~~(λ >>> λ) *)
  65   set (epic _ (iso_epic (pmon_cancelr ((a⊗b)⊗EI)))) as q.
  66     apply q.
  67     clear q.
  68
  69   (* next, we show that the hint goal above is implied by the bottom-left 1/5th of the big whiteboard diagram *)
  70   set (ni_commutes pmon_cancelr (α a b EI)) as q.
  71     setoid_rewrite <- associativity.
  72     setoid_rewrite q.
  73     clear q.
  74     setoid_rewrite associativity.
  75
  76     set (ni_commutes pmon_cancelr (a ⋊ #(pmon_cancelr b))) as q.
  77     simpl in q.
  78     setoid_rewrite q.
  79     clear q.
  80
  81     set (ni_commutes pmon_cancelr (#(pmon_cancelr (a⊗b)))) as q.
  82     simpl in q.
  83     setoid_rewrite q.
  84     clear q.
  85
  86     setoid_rewrite <- associativity.
  87     apply comp_respects; try reflexivity.
  88
  89   (* now we carry out the proof in the whiteboard diagram, starting from the pentagon diagram *)
  90
  91   (* top 2/5ths *)
  92   assert (α (a⊗b) EI EI >>> α _ _ _ >>> (_ ⋊ (_ ⋊ #(pmon_cancell _))) ~~ #(pmon_cancelr _) ⋉ _ >>> α _ _ _).
  93     set (pmon_triangle (a⊗b) EI) as tria.
  94     simpl in tria.
  95     unfold α; simpl.
  96     setoid_rewrite tria.
  97     clear tria.
  98     setoid_rewrite associativity.
  99     apply comp_respects; try reflexivity.
 100     set (ni_commutes (pmon_assoc_ll a b) #(pmon_cancell EI)) as x.
 101     simpl in x.
 102     setoid_rewrite pmon_coherent_l in x.
 103     apply x.
 104
 105   (* bottom 3/5ths *)
 106   assert (((#((pmon_assoc a EI) b) ⋉ EI >>> #((pmon_assoc a EI) (b ⊗ EI))) >>>
 107     a ⋊ #((pmon_assoc b EI) EI)) >>> a ⋊ (b ⋊ #(pmon_cancell EI))
 108     ~~ α _ _ _ ⋉ _ >>> (_ ⋊ #(pmon_cancelr _)) ⋉ _ >>> α _ _ _).
 109
 110     unfold α; simpl.
 111     repeat setoid_rewrite associativity.
 112     apply comp_respects; try reflexivity.
 113
 114     set (ni_commutes (pmon_assoc a EI) (#(pmon_cancelr b) )) as x.
 115     simpl in x.
 116     setoid_rewrite <- associativity.
 117     simpl in x.
 118     setoid_rewrite <- x.
 119     clear x.
 120
 121     setoid_rewrite associativity.
 122     apply comp_respects; try reflexivity.
 123     setoid_rewrite (fmor_preserves_comp (a⋊-)).
 124     apply (fmor_respects (a⋊-)).
 125
 126     set (pmon_triangle b EI) as tria.
 127     simpl in tria.
 128     symmetry.
 129     apply tria.
 130
 131   set (pmon_pentagon a b EI EI) as penta. unfold pmon_pentagon in penta. simpl in penta.
 132
 133   set (@comp_respects _ _ _ _ _ _ _ _ penta (a ⋊ (b ⋊ #(pmon_cancell EI))) (a ⋊ (b ⋊ #(pmon_cancell EI)))) as qq.
 134     unfold α in H.
 135     setoid_rewrite H in qq.
 136     unfold α in H0.
 137     setoid_rewrite H0 in qq.
 138     clear H0 H.
 139
 140   unfold α.
 141     apply (monic _ (iso_monic ((pmon_assoc a EI) b))).
 142     apply qq.
 143     clear qq penta.
 144     reflexivity.
 145     Qed.
 146
 147 Class PreMonoidalFunctor
 148 `(PM1:PreMonoidalCat(C:=C1)(I:=I1))
 149 `(PM2:PreMonoidalCat(C:=C2)(I:=I2))
 150  (fobj : C1 -> C2                 ) :=
 151 { mf_F          :> Functor C1 C2 fobj
 152 ; mf_i          :  I2 ≅ mf_F I1
 153 ; mf_first      :  ∀ a,              mf_F >>>> bin_first  (mf_F a)  <~~~>  bin_first  a >>>> mf_F
 154 ; mf_second     :  ∀ a,              mf_F >>>> bin_second (mf_F a)  <~~~>  bin_second a >>>> mf_F
 155 ; mf_consistent :  ∀ a b,            #(mf_first a b) ~~ #(mf_second b a)
 156 ; mf_center     :  forall `(f:a~>b), CentralMorphism f -> CentralMorphism (mf_F \ f)
 157 ; mf_cancell    :  ∀ b,     #(pmon_cancell _) ~~ #mf_i ⋉ _ >>> #(mf_first  b I1) >>> mf_F \ #(pmon_cancell b)
 158 ; mf_cancelr    :  ∀ a,     #(pmon_cancelr _) ~~ _ ⋊ #mf_i >>> #(mf_second a I1) >>> mf_F \ #(pmon_cancelr a)
 159 ; mf_assoc      :  ∀ a b c, #(pmon_assoc _ _ _)  >>> _ ⋊ #(mf_second _ _) >>>        #(mf_second _ _) ~~
 160                             #(mf_second _ _) ⋉ _ >>>     #(mf_second _ _) >>> mf_F \ #(pmon_assoc a c b)
 161 }.
 162 Coercion mf_F : PreMonoidalFunctor >-> Functor.
 163
 164 Section PreMonoidalFunctorsCompose.
 165   Context
 166   `{PM1   :PreMonoidalCat(C:=C1)(I:=I1)}
 167   `{PM2   :PreMonoidalCat(C:=C2)(I:=I2)}
 168    {fobj12:C1 -> C2                    }
 169    (PMF12 :PreMonoidalFunctor PM1 PM2 fobj12)
 170   `{PM3   :PreMonoidalCat(C:=C3)(I:=I3)}
 171    {fobj23:C2 -> C3                    }
 172    (PMF23 :PreMonoidalFunctor PM2 PM3 fobj23).
 173
 174   Definition compose_mf := PMF12 >>>> PMF23.
 175
 176   Definition compose_mf_i : I3 ≅ PMF23 (PMF12 I1).
 177     eapply iso_comp.
 178     apply (mf_i(PreMonoidalFunctor:=PMF23)).
 179     apply functors_preserve_isos.
 180     apply (mf_i(PreMonoidalFunctor:=PMF12)).
 181     Defined.
 182
 183   Definition compose_mf_first a : compose_mf >>>> bin_first (compose_mf a)  <~~~>  bin_first  a >>>> compose_mf.
 184     set (mf_first(PreMonoidalFunctor:=PMF12) a) as mf_first12.
 185     set (mf_first(PreMonoidalFunctor:=PMF23) (PMF12 a)) as mf_first23.
 186     unfold functor_fobj in *; simpl in *.
 187     unfold compose_mf.
 188     eapply ni_comp.
 189     apply (ni_associativity PMF12 PMF23 (- ⋉fobj23 (fobj12 a))).
 190     eapply ni_comp.
 191     apply (ni_respects PMF12 PMF12 (PMF23 >>>> - ⋉fobj23 (fobj12 a)) (- ⋉fobj12 a >>>> PMF23)).
 192     apply  ni_id.
 193     apply mf_first23.
 194     clear mf_first23.
 195
 196     eapply ni_comp.
 197     eapply ni_inv.
 198     apply (ni_associativity PMF12 (- ⋉fobj12 a) PMF23).
 199
 200     apply ni_inv.
 201     eapply ni_comp.
 202     eapply ni_inv.
 203     eapply (ni_associativity _ PMF12 PMF23).
 204
 205     apply ni_respects; [ idtac | apply ni_id ].
 206     apply ni_inv.
 207     apply mf_first12.
 208     Defined.
 209
 210   Definition compose_mf_second a : compose_mf >>>> bin_second (compose_mf a)  <~~~>  bin_second  a >>>> compose_mf.
 211     set (mf_second(PreMonoidalFunctor:=PMF12) a) as mf_second12.
 212     set (mf_second(PreMonoidalFunctor:=PMF23) (PMF12 a)) as mf_second23.
 213     unfold functor_fobj in *; simpl in *.
 214     unfold compose_mf.
 215     eapply ni_comp.
 216     apply (ni_associativity PMF12 PMF23 (fobj23 (fobj12 a) ⋊-)).
 217     eapply ni_comp.
 218     apply (ni_respects PMF12 PMF12 (PMF23 >>>> fobj23 (fobj12 a) ⋊-) (fobj12 a ⋊- >>>> PMF23)).
 219     apply  ni_id.
 220     apply mf_second23.
 221     clear mf_second23.
 222
 223     eapply ni_comp.
 224     eapply ni_inv.
 225     apply (ni_associativity PMF12 (fobj12 a ⋊ -) PMF23).
 226
 227     apply ni_inv.
 228     eapply ni_comp.
 229     eapply ni_inv.
 230     eapply (ni_associativity (a ⋊-) PMF12 PMF23).
 231
 232     apply ni_respects; [ idtac | apply ni_id ].
 233     apply ni_inv.
 234     apply mf_second12.
 235     Defined.
 236
 237   Lemma compose_assoc_coherence a b c :
 238    (#((pmon_assoc (compose_mf a) (fobj23 (fobj12 c))) (compose_mf b)) >>>
 239     compose_mf a ⋊ #((compose_mf_second b) c)) >>>
 240    #((compose_mf_second a) (b ⊗ c)) ~~
 241    (#((compose_mf_second a) b) ⋉ fobj23 (fobj12 c) >>>
 242     #((compose_mf_second (a ⊗ b)) c)) >>> compose_mf \ #((pmon_assoc a c) b).
 243 (*
 244       set (mf_assoc a b c) as x.
 245       set (mf_assoc (fobj12 a) (fobj12 b) (fobj12 c)) as x'.
 246       unfold functor_fobj in *.
 247       simpl in *.
 248       etransitivity.
 249       etransitivity.
 250       etransitivity.
 251       Focus 3.
 252       apply x'.
 253
 254       apply iso_shift_left' in x'.
 255
 256       unfold compose_mf_second; simpl.
 257       unfold functor_fobj; simpl.
 258       set (mf_second (fobj12 b)) as m.
 259       assert (mf_second (fobj12 b)=m). reflexivity.
 260       destruct m; simpl.
 261       setoid_rewrite <- fmor_preserves_comp.
 262       setoid_rewrite <- fmor_preserves_comp.
 263       setoid_rewrite <- fmor_preserves_comp.
 264       setoid_rewrite <- fmor_preserves_comp.
 265       setoid_rewrite <- fmor_preserves_comp.
 266       setoid_rewrite fmor_preserves_id.
 267       setoid_rewrite fmor_preserves_id.
 268       setoid_rewrite fmor_preserves_id.
 269       setoid_rewrite right_identity.
 270       setoid_rewrite left_identity.
 271       setoid_rewrite left_identity.
 272       setoid_rewrite left_identity.
 273
 274       set (mf_second (fobj12 (a ⊗ b))) as m''.
 275       assert (mf_second (fobj12 (a ⊗ b))=m''). reflexivity.
 276       destruct m''; simpl.
 277       unfold functor_fobj; simpl.
 278       setoid_rewrite fmor_preserves_id.
 279       setoid_rewrite fmor_preserves_id.
 280       setoid_rewrite right_identity.
 281       setoid_rewrite left_identity.
 282       setoid_rewrite left_identity.
 283       setoid_rewrite left_identity.
 284
 285       set (mf_second (fobj12 a)) as m'.
 286       assert (mf_second (fobj12 a)=m'). reflexivity.
 287       destruct m'; simpl.
 288       setoid_rewrite <- fmor_preserves_comp.
 289       setoid_rewrite <- fmor_preserves_comp.
 290       setoid_rewrite <- fmor_preserves_comp.
 291       setoid_rewrite <- fmor_preserves_comp.
 292       setoid_rewrite <- fmor_preserves_comp.
 293       setoid_rewrite    left_identity.
 294       setoid_rewrite    left_identity.
 295       setoid_rewrite    left_identity.
 296       setoid_rewrite    right_identity.
 297       assert (fobj23 (fobj12 a) ⋊ PMF23 \ id (PMF12 (b ⊗ c)) ~~ id _).
 298       (* *)
 299       setoid_rewrite H2.
 300       setoid_rewrite left_identity.
 301       assert ((id (fobj23 (fobj12 a) ⊗ fobj23 (fobj12 b)) ⋉ fobj23 (fobj12 c)) ~~ id _).
 302       (* *)
 303       setoid_rewrite H3.
 304       setoid_rewrite left_identity.
 305       assert (id (fobj23 (fobj12 a ⊗ fobj12 b)) ⋉ fobj23 (fobj12 c) ~~ id _).
 306       (* *)
 307         setoid_rewrite H4.
 308         setoid_rewrite left_identity.
 309         clear H4.
 310         setoid_rewrite left_identity.
 311       assert (id (fobj23 (fobj12 (a ⊗ b))) ⋉ fobj23 (fobj12 c) ~~ id _).
 312       (* *)
 313         setoid_rewrite H4.
 314         setoid_rewrite right_identity.
 315         clear H4.
 316       assert ((fobj23 (fobj12 a) ⋊ PMF23 \ id (PMF12 b)) ⋉ fobj23 (fobj12 c) ~~ id _).
 317       (* *)
 318         setoid_rewrite H4.
 319         setoid_rewrite left_identity.
 320         clear H4.
 321       unfold functor_comp in ni_commutes0; simpl in ni_commutes0.
 322       unfold functor_comp in ni_commutes;  simpl in ni_commutes.
 323       unfold functor_comp in ni_commutes1;  simpl in ni_commutes1.
 324
 325
 326       unfold functor_fobj in *.
 327       simpl in *.
 328       setoid_rewrite x in x'.
 329       rewrite H1.
 330       set (ni_commutes0 (a )
 331       setoid_rewrite fmor_preserves_id.
 332       etransitivity.
 333       eapply comp_respects.
 334       reflexivity.
 335       eapply comp_respects.
 336       eapply comp_respects.
 337         apply
 338       Focus 2.
 339       eapply fmor_preserves_id.
 340       setoid_rewrite    (fmor_preserves_id PMF23).
 341 *)
 342     admit.
 343     Qed.
 344
 345   Instance PreMonoidalFunctorsCompose : PreMonoidalFunctor PM1 PM3 (fobj23 ○ fobj12) :=
 346   { mf_i      := compose_mf_i
 347   ; mf_F      := compose_mf
 348   ; mf_first  := compose_mf_first
 349   ; mf_second := compose_mf_second }.
 350     intros; unfold compose_mf_first; unfold compose_mf_second.
 351       set (mf_first (PMF12 a)) as x in *.
 352       set (mf_second (PMF12 b)) as y in *.
 353       assert (x=mf_first (PMF12 a)). reflexivity.
 354       assert (y=mf_second (PMF12 b)). reflexivity.
 355       destruct x.
 356       destruct y.
 357       simpl.
 358       repeat setoid_rewrite left_identity.
 359       repeat setoid_rewrite right_identity.
 360       set (mf_consistent (PMF12 a) (PMF12 b)) as later.
 361       apply comp_respects; try reflexivity.
 362       unfold functor_comp.
 363       unfold functor_fobj; simpl.
 364       set (ni_commutes _ _ (id (fobj12 b))) as x.
 365       unfold functor_comp in x.
 366       simpl in x.
 367       unfold functor_fobj in x.
 368       symmetry in x.
 369       etransitivity.
 370       apply x.
 371       clear x.
 372       set (ni_commutes0 _ _ (id (fobj12 a))) as x'.
 373       unfold functor_comp in x'.
 374       simpl in x'.
 375       unfold functor_fobj in x'.
 376       etransitivity; [ idtac | apply x' ].
 377       clear x'.
 378       setoid_rewrite fmor_preserves_id.
 379       setoid_rewrite fmor_preserves_id.
 380       setoid_rewrite right_identity.
 381       rewrite <- H in later.
 382       rewrite <- H0 in later.
 383       simpl in later.
 384       apply later.
 385       apply fmor_respects.
 386       apply (mf_consistent a b).
 387
 388     intros.
 389       simpl.
 390       apply mf_center.
 391       apply mf_center.
 392       auto.
 393
 394     intros.
 395       unfold compose_mf_first; simpl.
 396       set (mf_first (PMF12 b)) as m.
 397       assert (mf_first (PMF12 b)=m). reflexivity.
 398       destruct m.
 399       simpl.
 400       unfold functor_fobj; simpl.
 401       repeat setoid_rewrite <- fmor_preserves_comp.
 402       repeat setoid_rewrite left_identity.
 403       repeat setoid_rewrite right_identity.
 404
 405       set (mf_cancell b) as y.
 406       set (mf_cancell (fobj12 b)) as y'.
 407       unfold functor_fobj in *.
 408       setoid_rewrite y in y'.
 409       clear y.
 410       setoid_rewrite <- fmor_preserves_comp in y'.
 411       setoid_rewrite <- fmor_preserves_comp in y'.
 412       etransitivity.
 413       apply y'.
 414       clear y'.
 415
 416       repeat setoid_rewrite <- associativity.
 417       apply comp_respects; try reflexivity.
 418       apply comp_respects; try reflexivity.
 419       repeat setoid_rewrite associativity.
 420       apply comp_respects; try reflexivity.
 421
 422       set (ni_commutes _ _ (id (fobj12 I1))) as x.
 423       unfold functor_comp in x.
 424       unfold functor_fobj in x.
 425       simpl in x.
 426       setoid_rewrite <- x.
 427       clear x.
 428       setoid_rewrite fmor_preserves_id.
 429       setoid_rewrite fmor_preserves_id.
 430       setoid_rewrite right_identity.
 431
 432       rewrite H.
 433       simpl.
 434       clear H.
 435       unfold functor_comp in ni_commutes.
 436       simpl in ni_commutes.
 437       apply ni_commutes.
 438
 439     intros.
 440       unfold compose_mf_second; simpl.
 441       set (mf_second (PMF12 a)) as m.
 442       assert (mf_second (PMF12 a)=m). reflexivity.
 443       destruct m.
 444       simpl.
 445       unfold functor_fobj; simpl.
 446       repeat setoid_rewrite <- fmor_preserves_comp.
 447       repeat setoid_rewrite left_identity.
 448       repeat setoid_rewrite right_identity.
 449
 450       set (mf_cancelr a) as y.
 451       set (mf_cancelr (fobj12 a)) as y'.
 452       unfold functor_fobj in *.
 453       setoid_rewrite y in y'.
 454       clear y.
 455       setoid_rewrite <- fmor_preserves_comp in y'.
 456       setoid_rewrite <- fmor_preserves_comp in y'.
 457       etransitivity.
 458       apply y'.
 459       clear y'.
 460
 461       repeat setoid_rewrite <- associativity.
 462       apply comp_respects; try reflexivity.
 463       apply comp_respects; try reflexivity.
 464       repeat setoid_rewrite associativity.
 465       apply comp_respects; try reflexivity.
 466
 467       set (ni_commutes _ _ (id (fobj12 I1))) as x.
 468       unfold functor_comp in x.
 469       unfold functor_fobj in x.
 470       simpl in x.
 471       setoid_rewrite <- x.
 472       clear x.
 473       setoid_rewrite fmor_preserves_id.
 474       setoid_rewrite fmor_preserves_id.
 475       setoid_rewrite right_identity.
 476
 477       rewrite H.
 478       simpl.
 479       clear H.
 480       unfold functor_comp in ni_commutes.
 481       simpl in ni_commutes.
 482       apply ni_commutes.
 483
 484     apply compose_assoc_coherence.
 485       Defined.
 486
 487 End PreMonoidalFunctorsCompose.
 488
 489
 490 (*******************************************************************************)
 491 (* Braided and Symmetric Categories                                            *)
 492
 493 Class BraidedCat `(mc:PreMonoidalCat) :=
 494 { br_niso        : forall a, bin_first a <~~~> bin_second a
 495 ; br_swap        := fun a b => ni_iso (br_niso b) a
 496 ; triangleb      : forall a:C,     #(pmon_cancelr a) ~~ #(br_swap a (pmon_I(PreMonoidalCat:=mc))) >>> #(pmon_cancell a)
 497 ; hexagon1       : forall {a b c}, #(pmon_assoc _ _ _) >>> #(br_swap a _) >>> #(pmon_assoc _ _ _)
 498                                    ~~ #(br_swap _ _) ⋉ c >>> #(pmon_assoc _ _ _) >>> b ⋊ #(br_swap _ _)
 499 ; hexagon2       : forall {a b c}, #(pmon_assoc _ _ _)⁻¹ >>> #(br_swap _ c) >>> #(pmon_assoc _ _ _)⁻¹
 500                                    ~~ a ⋊ #(br_swap _ _) >>> #(pmon_assoc _ _ _)⁻¹ >>> #(br_swap _ _) ⋉ b
 501 }.
 502
 503 Class SymmetricCat `(bc:BraidedCat) :=
 504 { symcat_swap  :  forall a b:C, #((br_swap(BraidedCat:=bc)) a b) ~~ #(br_swap _ _)⁻¹
 505 }.
 506
 507
 508 (* a wide subcategory inherits the premonoidal structure if it includes all of the coherence maps *)
 509 Section PreMonoidalWideSubcategory.
 510
 511   Context `(pm:PreMonoidalCat(I:=pmI)).
 512   Context  {Pmor}(S:WideSubcategory pm Pmor).
 513   Context  (Pmor_first  : forall {a}{b}{c}{f}(pf:Pmor a b f), Pmor _ _ (f ⋉ c)).
 514   Context  (Pmor_second : forall {a}{b}{c}{f}(pf:Pmor a b f), Pmor _ _ (c ⋊ f)).
 515   Context  (Pmor_assoc  : forall {a}{b}{c}, Pmor _ _ #(pmon_assoc a c b)).
 516   Context  (Pmor_unassoc: forall {a}{b}{c}, Pmor _ _ #(pmon_assoc a c b)⁻¹).
 517   Context  (Pmor_cancell: forall {a}, Pmor _ _ #(pmon_cancell a)).
 518   Context  (Pmor_uncancell: forall {a}, Pmor _ _ #(pmon_cancell a)⁻¹).
 519   Context  (Pmor_cancelr: forall {a}, Pmor _ _ #(pmon_cancelr a)).
 520   Context  (Pmor_uncancelr: forall {a}, Pmor _ _ #(pmon_cancelr a)⁻¹).
 521   Implicit Arguments Pmor_first [[a][b][c][f]].
 522   Implicit Arguments Pmor_second [[a][b][c][f]].
 523
 524   Definition PreMonoidalWideSubcategory_first_fmor (a:S) : forall {x}{y}(f:x~~{S}~~>y), (bin_obj' x a)~~{S}~~>(bin_obj' y a).
 525     unfold hom; simpl; intros.
 526     destruct f.
 527     simpl in *.
 528     exists (bin_first(BinoidalCat:=pm) a \ x0).
 529     apply Pmor_first; auto.
 530     Defined.
 531
 532   Definition PreMonoidalWideSubcategory_second_fmor (a:S) : forall {x}{y}(f:x~~{S}~~>y), (bin_obj' a x)~~{S}~~>(bin_obj' a y).
 533     unfold hom; simpl; intros.
 534     destruct f.
 535     simpl in *.
 536     exists (bin_second(BinoidalCat:=pm) a \ x0).
 537     apply Pmor_second; auto.
 538     Defined.
 539
 540   Instance PreMonoidalWideSubcategory_first (a:S) : Functor S S (fun x => bin_obj' x a) :=
 541     { fmor := fun x y f => PreMonoidalWideSubcategory_first_fmor a f }.
 542     unfold PreMonoidalWideSubcategory_first_fmor; intros; destruct f; destruct f'; simpl in *.
 543     apply (fmor_respects (bin_first(BinoidalCat:=pm) a)); auto.
 544     unfold PreMonoidalWideSubcategory_first_fmor; intros; simpl in *.
 545     apply (fmor_preserves_id (bin_first(BinoidalCat:=pm) a)); auto.
 546     unfold PreMonoidalWideSubcategory_first_fmor; intros; destruct f; destruct g; simpl in *.
 547     apply (fmor_preserves_comp (bin_first(BinoidalCat:=pm) a)); auto.
 548     Defined.
 549
 550   Instance PreMonoidalWideSubcategory_second (a:S) : Functor S S (fun x => bin_obj' a x) :=
 551     { fmor := fun x y f => PreMonoidalWideSubcategory_second_fmor a f }.
 552     unfold PreMonoidalWideSubcategory_second_fmor; intros; destruct f; destruct f'; simpl in *.
 553     apply (fmor_respects (bin_second(BinoidalCat:=pm) a)); auto.
 554     unfold PreMonoidalWideSubcategory_second_fmor; intros; simpl in *.
 555     apply (fmor_preserves_id (bin_second(BinoidalCat:=pm) a)); auto.
 556     unfold PreMonoidalWideSubcategory_second_fmor; intros; destruct f; destruct g; simpl in *.
 557     apply (fmor_preserves_comp (bin_second(BinoidalCat:=pm) a)); auto.
 558     Defined.
 559
 560   Instance PreMonoidalWideSubcategory_is_Binoidal : BinoidalCat S bin_obj' :=
 561     { bin_first  := PreMonoidalWideSubcategory_first
 562     ; bin_second := PreMonoidalWideSubcategory_second }.
 563
 564   Definition PreMonoidalWideSubcategory_assoc_iso
 565     : forall a b c, Isomorphic(C:=S) (bin_obj' (bin_obj' a b) c) (bin_obj' a (bin_obj' b c)).
 566     intros.
 567     refine {| iso_forward := existT _ _ (Pmor_assoc a b c) ; iso_backward := existT _ _ (Pmor_unassoc a b c) |}.
 568     simpl; apply iso_comp1.
 569     simpl; apply iso_comp2.
 570     Defined.
 571
 572   Definition PreMonoidalWideSubcategory_assoc
 573     : forall a b,
 574       (PreMonoidalWideSubcategory_second a >>>> PreMonoidalWideSubcategory_first b) <~~~>
 575       (PreMonoidalWideSubcategory_first  b >>>> PreMonoidalWideSubcategory_second a).
 576     intros.
 577     apply (@Build_NaturalIsomorphism _ _ _ _ _ _ _ _ (PreMonoidalWideSubcategory_second a >>>>
 578       PreMonoidalWideSubcategory_first b) (PreMonoidalWideSubcategory_first b >>>>
 579         PreMonoidalWideSubcategory_second a) (fun c => PreMonoidalWideSubcategory_assoc_iso a c b)).
 580     intros; simpl.
 581     unfold PreMonoidalWideSubcategory_second_fmor; simpl.
 582     destruct f; simpl.
 583     set (ni_commutes (pmon_assoc(PreMonoidalCat:=pm) a b) x) as q.
 584     apply q.
 585     Defined.
 586
 587   Definition PreMonoidalWideSubcategory_assoc_ll
 588     : forall a b,
 589       PreMonoidalWideSubcategory_second (a⊗b) <~~~>
 590       PreMonoidalWideSubcategory_second b >>>> PreMonoidalWideSubcategory_second a.
 591     intros.
 592     apply (@Build_NaturalIsomorphism _ _ _ _ _ _ _ _
 593              (PreMonoidalWideSubcategory_second (a⊗b))
 594              (PreMonoidalWideSubcategory_second b >>>> PreMonoidalWideSubcategory_second a)
 595              (fun c => PreMonoidalWideSubcategory_assoc_iso a b c)).
 596     intros; simpl.
 597     unfold PreMonoidalWideSubcategory_second_fmor; simpl.
 598     destruct f; simpl.
 599     set (ni_commutes (pmon_assoc_ll(PreMonoidalCat:=pm) a b) x) as q.
 600     unfold functor_comp in q; simpl in q.
 601     set (pmon_coherent_l(PreMonoidalCat:=pm)) as q'.
 602     setoid_rewrite q' in q.
 603     apply q.
 604     Defined.
 605
 606   Definition PreMonoidalWideSubcategory_assoc_rr
 607     : forall a b,
 608       PreMonoidalWideSubcategory_first (a⊗b) <~~~>
 609       PreMonoidalWideSubcategory_first a >>>> PreMonoidalWideSubcategory_first b.
 610     intros.
 611     apply ni_inv.
 612     apply (@Build_NaturalIsomorphism _ _ _ _ _ _ _ _
 613              (PreMonoidalWideSubcategory_first a >>>> PreMonoidalWideSubcategory_first b)
 614              (PreMonoidalWideSubcategory_first (a⊗b))
 615              (fun c => PreMonoidalWideSubcategory_assoc_iso c a b)).
 616     intros; simpl.
 617     unfold PreMonoidalWideSubcategory_second_fmor; simpl.
 618     destruct f; simpl.
 619     set (ni_commutes (pmon_assoc_rr(PreMonoidalCat:=pm) a b) x) as q.
 620     unfold functor_comp in q; simpl in q.
 621     set (pmon_coherent_r(PreMonoidalCat:=pm)) as q'.
 622     setoid_rewrite q' in q.
 623     apply iso_shift_right' in q.
 624     apply iso_shift_left.
 625     symmetry.
 626     setoid_rewrite iso_inv_inv in q.
 627     setoid_rewrite associativity.
 628     apply q.
 629     Defined.
 630
 631   Definition PreMonoidalWideSubcategory_cancelr_iso : forall a, Isomorphic(C:=S) (bin_obj' a pmI) a.
 632     intros.
 633     refine {| iso_forward := existT _ _ (Pmor_cancelr a) ; iso_backward := existT _ _ (Pmor_uncancelr a) |}.
 634     simpl; apply iso_comp1.
 635     simpl; apply iso_comp2.
 636     Defined.
 637
 638   Definition PreMonoidalWideSubcategory_cancell_iso : forall a, Isomorphic(C:=S) (bin_obj' pmI a) a.
 639     intros.
 640     refine {| iso_forward := existT _ _ (Pmor_cancell a) ; iso_backward := existT _ _ (Pmor_uncancell a) |}.
 641     simpl; apply iso_comp1.
 642     simpl; apply iso_comp2.
 643     Defined.
 644
 645   Definition PreMonoidalWideSubcategory_cancelr : PreMonoidalWideSubcategory_first pmI <~~~> functor_id _.
 646     apply (@Build_NaturalIsomorphism _ _ _ _ _ _ _ _
 647              (PreMonoidalWideSubcategory_first pmI) (functor_id _) PreMonoidalWideSubcategory_cancelr_iso).
 648     intros; simpl.
 649     unfold PreMonoidalWideSubcategory_first_fmor; simpl.
 650     destruct f; simpl.
 651     apply (ni_commutes (pmon_cancelr(PreMonoidalCat:=pm)) x).
 652     Defined.
 653
 654   Definition PreMonoidalWideSubcategory_cancell : PreMonoidalWideSubcategory_second pmI <~~~> functor_id _.
 655     apply (@Build_NaturalIsomorphism _ _ _ _ _ _ _ _
 656              (PreMonoidalWideSubcategory_second pmI) (functor_id _) PreMonoidalWideSubcategory_cancell_iso).
 657     intros; simpl.
 658     unfold PreMonoidalWideSubcategory_second_fmor; simpl.
 659     destruct f; simpl.
 660     apply (ni_commutes (pmon_cancell(PreMonoidalCat:=pm)) x).
 661     Defined.
 662
 663   Instance PreMonoidalWideSubcategory_PreMonoidal : PreMonoidalCat PreMonoidalWideSubcategory_is_Binoidal pmI :=
 664   { pmon_assoc           := PreMonoidalWideSubcategory_assoc
 665   ; pmon_assoc_rr        := PreMonoidalWideSubcategory_assoc_rr
 666   ; pmon_assoc_ll        := PreMonoidalWideSubcategory_assoc_ll
 667   ; pmon_cancelr         := PreMonoidalWideSubcategory_cancelr
 668   ; pmon_cancell         := PreMonoidalWideSubcategory_cancell
 669   }.
 670   apply Build_Pentagon.
 671     intros; unfold PreMonoidalWideSubcategory_assoc; simpl.
 672     set (pmon_pentagon(PreMonoidalCat:=pm) a b c) as q.
 673     simpl in q.
 674     apply q.
 675   apply Build_Triangle.
 676     intros; unfold PreMonoidalWideSubcategory_assoc;
 677       unfold PreMonoidalWideSubcategory_cancelr; unfold PreMonoidalWideSubcategory_cancell; simpl.
 678     set (pmon_triangle(PreMonoidalCat:=pm) a b) as q.
 679     simpl in q.
 680     apply q.
 681     intros.
 682
 683   set (pmon_triangle(PreMonoidalCat:=pm)) as q.
 684     apply q.
 685
 686   intros; simpl; reflexivity.
 687   intros; simpl; reflexivity.
 688
 689   intros; simpl.
 690     apply Build_CentralMorphism; intros; simpl; destruct g; simpl.
 691     apply (pmon_assoc_central(PreMonoidalCat:=pm) a b c).
 692     apply (pmon_assoc_central(PreMonoidalCat:=pm) a b c).
 693
 694   intros; simpl.
 695     apply Build_CentralMorphism; intros; simpl; destruct g; simpl.
 696     apply (pmon_cancelr_central(PreMonoidalCat:=pm) a).
 697     apply (pmon_cancelr_central(PreMonoidalCat:=pm) a).
 698
 699   intros; simpl.
 700     apply Build_CentralMorphism; intros; simpl; destruct g; simpl.
 701     apply (pmon_cancell_central(PreMonoidalCat:=pm) a).
 702     apply (pmon_cancell_central(PreMonoidalCat:=pm) a).
 703     Defined.
 704
 705 End PreMonoidalWideSubcategory.
 706
 707
 708 (* a full subcategory inherits the premonoidal structure if it includes the unit object and is closed under object-pairing *)
 709 (*
 710 Section PreMonoidalFullSubcategory.
 711
 712   Context `(pm:PreMonoidalCat(I:=pmI)).
 713   Context  {Pobj}(S:FullSubcategory pm Pobj).
 714   Context  (Pobj_unit:Pobj pmI).
 715   Context  (Pobj_closed:forall {a}{b}, Pobj a -> Pobj b -> Pobj (a⊗b)).
 716   Implicit Arguments Pobj_closed [[a][b]].
 717
 718   Definition PreMonoidalFullSubcategory_bobj (x y:S) :=
 719     existT Pobj _ (Pobj_closed (projT2 x) (projT2 y)).
 720
 721   Definition PreMonoidalFullSubcategory_first_fmor (a:S) : forall {x}{y}(f:x~~{S}~~>y),
 722     (PreMonoidalFullSubcategory_bobj x a)~~{S}~~>(PreMonoidalFullSubcategory_bobj y a).
 723     unfold hom; simpl; intros.
 724     destruct a as [a apf].
 725     destruct x as [x xpf].
 726     destruct y as [y ypf].
 727     simpl in *.
 728     apply (f ⋉ a).
 729     Defined.
 730
 731   Definition PreMonoidalFullSubcategory_second_fmor (a:S) : forall {x}{y}(f:x~~{S}~~>y),
 732     (PreMonoidalFullSubcategory_bobj a x)~~{S}~~>(PreMonoidalFullSubcategory_bobj a y).
 733     unfold hom; simpl; intros.
 734     destruct a as [a apf].
 735     destruct x as [x xpf].
 736     destruct y as [y ypf].
 737     simpl in *.
 738     apply (a ⋊ f).
 739     Defined.
 740
 741   Instance PreMonoidalFullSubcategory_first (a:S)
 742     : Functor S S (fun x => PreMonoidalFullSubcategory_bobj x a) :=
 743     { fmor := fun x y f => PreMonoidalFullSubcategory_first_fmor a f }.
 744     unfold PreMonoidalFullSubcategory_first_fmor; intros; destruct a; destruct a0; destruct b; simpl in *.
 745     apply (fmor_respects (-⋉x)); auto.
 746     unfold PreMonoidalFullSubcategory_first_fmor; intros; destruct a; destruct a0;  simpl in *.
 747     apply (fmor_preserves_id (-⋉x)); auto.
 748     unfold PreMonoidalFullSubcategory_first_fmor; intros;
 749       destruct a; destruct a0; destruct b; destruct c; simpl in *.
 750     apply (fmor_preserves_comp (-⋉x)); auto.
 751     Defined.
 752
 753   Instance PreMonoidalFullSubcategory_second (a:S)
 754     : Functor S S (fun x => PreMonoidalFullSubcategory_bobj a x) :=
 755     { fmor := fun x y f => PreMonoidalFullSubcategory_second_fmor a f }.
 756     unfold PreMonoidalFullSubcategory_second_fmor; intros; destruct a; destruct a0; destruct b; simpl in *.
 757     apply (fmor_respects (x⋊-)); auto.
 758     unfold PreMonoidalFullSubcategory_second_fmor; intros; destruct a; destruct a0;  simpl in *.
 759     apply (fmor_preserves_id (x⋊-)); auto.
 760     unfold PreMonoidalFullSubcategory_second_fmor; intros;
 761       destruct a; destruct a0; destruct b; destruct c; simpl in *.
 762     apply (fmor_preserves_comp (x⋊-)); auto.
 763     Defined.
 764
 765   Instance PreMonoidalFullSubcategory_is_Binoidal : BinoidalCat S PreMonoidalFullSubcategory_bobj :=
 766     { bin_first := PreMonoidalFullSubcategory_first
 767     ; bin_second := PreMonoidalFullSubcategory_second }.
 768
 769   Definition PreMonoidalFullSubcategory_assoc
 770     : forall a b,
 771       (PreMonoidalFullSubcategory_second a >>>> PreMonoidalFullSubcategory_first b) <~~~>
 772       (PreMonoidalFullSubcategory_first  b >>>> PreMonoidalFullSubcategory_second a).
 773     Defined.
 774
 775   Definition PreMonoidalFullSubcategory_assoc_ll
 776     : forall a b,
 777       PreMonoidalFullSubcategory_second (a⊗b) <~~~>
 778       PreMonoidalFullSubcategory_second b >>>> PreMonoidalFullSubcategory_second a.
 779     intros.
 780     Defined.
 781
 782   Definition PreMonoidalFullSubcategory_assoc_rr
 783     : forall a b,
 784       PreMonoidalFullSubcategory_first (a⊗b) <~~~>
 785       PreMonoidalFullSubcategory_first a >>>> PreMonoidalFullSubcategory_first b.
 786     intros.
 787     Defined.
 788
 789   Definition PreMonoidalFullSubcategory_I := existT _ pmI Pobj_unit.
 790
 791   Definition PreMonoidalFullSubcategory_cancelr
 792     : PreMonoidalFullSubcategory_first PreMonoidalFullSubcategory_I <~~~> functor_id _.
 793     Defined.
 794
 795   Definition PreMonoidalFullSubcategory_cancell
 796     : PreMonoidalFullSubcategory_second PreMonoidalFullSubcategory_I <~~~> functor_id _.
 797     Defined.
 798
 799   Instance PreMonoidalFullSubcategory_PreMonoidal
 800     : PreMonoidalCat PreMonoidalFullSubcategory_is_Binoidal PreMonoidalFullSubcategory_I :=
 801   { pmon_assoc           := PreMonoidalFullSubcategory_assoc
 802   ; pmon_assoc_rr        := PreMonoidalFullSubcategory_assoc_rr
 803   ; pmon_assoc_ll        := PreMonoidalFullSubcategory_assoc_ll
 804   ; pmon_cancelr         := PreMonoidalFullSubcategory_cancelr
 805   ; pmon_cancell         := PreMonoidalFullSubcategory_cancell
 806   }.
 807   Defined.
 808 End PreMonoidalFullSubcategory.
 809 *)