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