src/PreMonoidalCategories.v

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