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