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