+
+
+(* a wide subcategory inherits the premonoidal structure if it includes all of the coherence maps *)
+Section PreMonoidalWideSubcategory.
+
+ Context `(pm:PreMonoidalCat(I:=pmI)).
+ Context {Pmor}(S:WideSubcategory pm Pmor).
+ Context (Pmor_first : forall {a}{b}{c}{f}(pf:Pmor a b f), Pmor _ _ (f ⋉ c)).
+ Context (Pmor_second : forall {a}{b}{c}{f}(pf:Pmor a b f), Pmor _ _ (c ⋊ f)).
+ Context (Pmor_assoc : forall {a}{b}{c}, Pmor _ _ #(pmon_assoc a c b)).
+ Context (Pmor_unassoc: forall {a}{b}{c}, Pmor _ _ #(pmon_assoc a c b)⁻¹).
+ Context (Pmor_cancell: forall {a}, Pmor _ _ #(pmon_cancell a)).
+ Context (Pmor_uncancell: forall {a}, Pmor _ _ #(pmon_cancell a)⁻¹).
+ Context (Pmor_cancelr: forall {a}, Pmor _ _ #(pmon_cancelr a)).
+ Context (Pmor_uncancelr: forall {a}, Pmor _ _ #(pmon_cancelr a)⁻¹).
+ Implicit Arguments Pmor_first [[a][b][c][f]].
+ Implicit Arguments Pmor_second [[a][b][c][f]].
+
+ Definition PreMonoidalWideSubcategory_first_fmor (a:S) : forall {x}{y}(f:x~~{S}~~>y), (bin_obj' x a)~~{S}~~>(bin_obj' y a).
+ unfold hom; simpl; intros.
+ destruct f.
+ simpl in *.
+ exists (bin_first(BinoidalCat:=pm) a \ x0).
+ apply Pmor_first; auto.
+ Defined.
+
+ Definition PreMonoidalWideSubcategory_second_fmor (a:S) : forall {x}{y}(f:x~~{S}~~>y), (bin_obj' a x)~~{S}~~>(bin_obj' a y).
+ unfold hom; simpl; intros.
+ destruct f.
+ simpl in *.
+ exists (bin_second(BinoidalCat:=pm) a \ x0).
+ apply Pmor_second; auto.
+ Defined.
+
+ Instance PreMonoidalWideSubcategory_first (a:S) : Functor S S (fun x => bin_obj' x a) :=
+ { fmor := fun x y f => PreMonoidalWideSubcategory_first_fmor a f }.
+ unfold PreMonoidalWideSubcategory_first_fmor; intros; destruct f; destruct f'; simpl in *.
+ apply (fmor_respects (bin_first(BinoidalCat:=pm) a)); auto.
+ unfold PreMonoidalWideSubcategory_first_fmor; intros; simpl in *.
+ apply (fmor_preserves_id (bin_first(BinoidalCat:=pm) a)); auto.
+ unfold PreMonoidalWideSubcategory_first_fmor; intros; destruct f; destruct g; simpl in *.
+ apply (fmor_preserves_comp (bin_first(BinoidalCat:=pm) a)); auto.
+ Defined.
+
+ Instance PreMonoidalWideSubcategory_second (a:S) : Functor S S (fun x => bin_obj' a x) :=
+ { fmor := fun x y f => PreMonoidalWideSubcategory_second_fmor a f }.
+ unfold PreMonoidalWideSubcategory_second_fmor; intros; destruct f; destruct f'; simpl in *.
+ apply (fmor_respects (bin_second(BinoidalCat:=pm) a)); auto.
+ unfold PreMonoidalWideSubcategory_second_fmor; intros; simpl in *.
+ apply (fmor_preserves_id (bin_second(BinoidalCat:=pm) a)); auto.
+ unfold PreMonoidalWideSubcategory_second_fmor; intros; destruct f; destruct g; simpl in *.
+ apply (fmor_preserves_comp (bin_second(BinoidalCat:=pm) a)); auto.
+ Defined.
+
+ Instance PreMonoidalWideSubcategory_is_Binoidal : BinoidalCat S bin_obj' :=
+ { bin_first := PreMonoidalWideSubcategory_first
+ ; bin_second := PreMonoidalWideSubcategory_second }.
+
+ Definition PreMonoidalWideSubcategory_assoc_iso
+ : forall a b c, Isomorphic(C:=S) (bin_obj' (bin_obj' a b) c) (bin_obj' a (bin_obj' b c)).
+ intros.
+ refine {| iso_forward := existT _ _ (Pmor_assoc a b c) ; iso_backward := existT _ _ (Pmor_unassoc a b c) |}.
+ simpl; apply iso_comp1.
+ simpl; apply iso_comp2.
+ Defined.
+
+ Definition PreMonoidalWideSubcategory_assoc
+ : forall a b,
+ (PreMonoidalWideSubcategory_second a >>>> PreMonoidalWideSubcategory_first b) <~~~>
+ (PreMonoidalWideSubcategory_first b >>>> PreMonoidalWideSubcategory_second a).
+ intros.
+ apply (@Build_NaturalIsomorphism _ _ _ _ _ _ _ _ (PreMonoidalWideSubcategory_second a >>>>
+ PreMonoidalWideSubcategory_first b) (PreMonoidalWideSubcategory_first b >>>>
+ PreMonoidalWideSubcategory_second a) (fun c => PreMonoidalWideSubcategory_assoc_iso a c b)).
+ intros; simpl.
+ unfold PreMonoidalWideSubcategory_second_fmor; simpl.
+ destruct f; simpl.
+ set (ni_commutes (pmon_assoc(PreMonoidalCat:=pm) a b) x) as q.
+ apply q.
+ Defined.
+
+ Definition PreMonoidalWideSubcategory_assoc_ll
+ : forall a b,
+ PreMonoidalWideSubcategory_second (a⊗b) <~~~>
+ PreMonoidalWideSubcategory_second b >>>> PreMonoidalWideSubcategory_second a.
+ intros.
+ apply (@Build_NaturalIsomorphism _ _ _ _ _ _ _ _
+ (PreMonoidalWideSubcategory_second (a⊗b))
+ (PreMonoidalWideSubcategory_second b >>>> PreMonoidalWideSubcategory_second a)
+ (fun c => PreMonoidalWideSubcategory_assoc_iso a b c)).
+ intros; simpl.
+ unfold PreMonoidalWideSubcategory_second_fmor; simpl.
+ destruct f; simpl.
+ set (ni_commutes (pmon_assoc_ll(PreMonoidalCat:=pm) a b) x) as q.
+ unfold functor_comp in q; simpl in q.
+ set (pmon_coherent_l(PreMonoidalCat:=pm)) as q'.
+ setoid_rewrite q' in q.
+ apply q.
+ Defined.
+
+ Definition PreMonoidalWideSubcategory_assoc_rr
+ : forall a b,
+ PreMonoidalWideSubcategory_first (a⊗b) <~~~>
+ PreMonoidalWideSubcategory_first a >>>> PreMonoidalWideSubcategory_first b.
+ intros.
+ apply ni_inv.
+ apply (@Build_NaturalIsomorphism _ _ _ _ _ _ _ _
+ (PreMonoidalWideSubcategory_first a >>>> PreMonoidalWideSubcategory_first b)
+ (PreMonoidalWideSubcategory_first (a⊗b))
+ (fun c => PreMonoidalWideSubcategory_assoc_iso c a b)).
+ intros; simpl.
+ unfold PreMonoidalWideSubcategory_second_fmor; simpl.
+ destruct f; simpl.
+ set (ni_commutes (pmon_assoc_rr(PreMonoidalCat:=pm) a b) x) as q.
+ unfold functor_comp in q; simpl in q.
+ set (pmon_coherent_r(PreMonoidalCat:=pm)) as q'.
+ setoid_rewrite q' in q.
+ apply iso_shift_right' in q.
+ apply iso_shift_left.
+ symmetry.
+ setoid_rewrite iso_inv_inv in q.
+ setoid_rewrite associativity.
+ apply q.
+ Defined.
+
+ Definition PreMonoidalWideSubcategory_cancelr_iso : forall a, Isomorphic(C:=S) (bin_obj' a pmI) a.
+ intros.
+ refine {| iso_forward := existT _ _ (Pmor_cancelr a) ; iso_backward := existT _ _ (Pmor_uncancelr a) |}.
+ simpl; apply iso_comp1.
+ simpl; apply iso_comp2.
+ Defined.
+
+ Definition PreMonoidalWideSubcategory_cancell_iso : forall a, Isomorphic(C:=S) (bin_obj' pmI a) a.
+ intros.
+ refine {| iso_forward := existT _ _ (Pmor_cancell a) ; iso_backward := existT _ _ (Pmor_uncancell a) |}.
+ simpl; apply iso_comp1.
+ simpl; apply iso_comp2.
+ Defined.
+
+ Definition PreMonoidalWideSubcategory_cancelr : PreMonoidalWideSubcategory_first pmI <~~~> functor_id _.
+ apply (@Build_NaturalIsomorphism _ _ _ _ _ _ _ _
+ (PreMonoidalWideSubcategory_first pmI) (functor_id _) PreMonoidalWideSubcategory_cancelr_iso).
+ intros; simpl.
+ unfold PreMonoidalWideSubcategory_first_fmor; simpl.
+ destruct f; simpl.
+ apply (ni_commutes (pmon_cancelr(PreMonoidalCat:=pm)) x).
+ Defined.
+
+ Definition PreMonoidalWideSubcategory_cancell : PreMonoidalWideSubcategory_second pmI <~~~> functor_id _.
+ apply (@Build_NaturalIsomorphism _ _ _ _ _ _ _ _
+ (PreMonoidalWideSubcategory_second pmI) (functor_id _) PreMonoidalWideSubcategory_cancell_iso).
+ intros; simpl.
+ unfold PreMonoidalWideSubcategory_second_fmor; simpl.
+ destruct f; simpl.
+ apply (ni_commutes (pmon_cancell(PreMonoidalCat:=pm)) x).
+ Defined.
+
+ Instance PreMonoidalWideSubcategory_PreMonoidal : PreMonoidalCat PreMonoidalWideSubcategory_is_Binoidal pmI :=
+ { pmon_assoc := PreMonoidalWideSubcategory_assoc
+ ; pmon_assoc_rr := PreMonoidalWideSubcategory_assoc_rr
+ ; pmon_assoc_ll := PreMonoidalWideSubcategory_assoc_ll
+ ; pmon_cancelr := PreMonoidalWideSubcategory_cancelr
+ ; pmon_cancell := PreMonoidalWideSubcategory_cancell
+ }.
+ apply Build_Pentagon.
+ intros; unfold PreMonoidalWideSubcategory_assoc; simpl.
+ set (pmon_pentagon(PreMonoidalCat:=pm) a b c) as q.
+ simpl in q.
+ apply q.
+ apply Build_Triangle.
+ intros; unfold PreMonoidalWideSubcategory_assoc;
+ unfold PreMonoidalWideSubcategory_cancelr; unfold PreMonoidalWideSubcategory_cancell; simpl.
+ set (pmon_triangle(PreMonoidalCat:=pm) a b) as q.
+ simpl in q.
+ apply q.
+ intros.
+
+ set (pmon_triangle(PreMonoidalCat:=pm)) as q.
+ apply q.
+
+ intros; simpl; reflexivity.
+ intros; simpl; reflexivity.
+
+ intros; simpl.
+ apply Build_CentralMorphism; intros; simpl; destruct g; simpl.
+ apply (pmon_assoc_central(PreMonoidalCat:=pm) a b c).
+ apply (pmon_assoc_central(PreMonoidalCat:=pm) a b c).
+
+ intros; simpl.
+ apply Build_CentralMorphism; intros; simpl; destruct g; simpl.
+ apply (pmon_cancelr_central(PreMonoidalCat:=pm) a).
+ apply (pmon_cancelr_central(PreMonoidalCat:=pm) a).
+
+ intros; simpl.
+ apply Build_CentralMorphism; intros; simpl; destruct g; simpl.
+ apply (pmon_cancell_central(PreMonoidalCat:=pm) a).
+ apply (pmon_cancell_central(PreMonoidalCat:=pm) a).
+ Defined.
+
+End PreMonoidalWideSubcategory.
+
+
+(* a full subcategory inherits the premonoidal structure if it includes the unit object and is closed under object-pairing *)
+(*
+Section PreMonoidalFullSubcategory.
+
+ Context `(pm:PreMonoidalCat(I:=pmI)).
+ Context {Pobj}(S:FullSubcategory pm Pobj).
+ Context (Pobj_unit:Pobj pmI).
+ Context (Pobj_closed:forall {a}{b}, Pobj a -> Pobj b -> Pobj (a⊗b)).
+ Implicit Arguments Pobj_closed [[a][b]].
+
+ Definition PreMonoidalFullSubcategory_bobj (x y:S) :=
+ existT Pobj _ (Pobj_closed (projT2 x) (projT2 y)).
+
+ Definition PreMonoidalFullSubcategory_first_fmor (a:S) : forall {x}{y}(f:x~~{S}~~>y),
+ (PreMonoidalFullSubcategory_bobj x a)~~{S}~~>(PreMonoidalFullSubcategory_bobj y a).
+ unfold hom; simpl; intros.
+ destruct a as [a apf].
+ destruct x as [x xpf].
+ destruct y as [y ypf].
+ simpl in *.
+ apply (f ⋉ a).
+ Defined.
+
+ Definition PreMonoidalFullSubcategory_second_fmor (a:S) : forall {x}{y}(f:x~~{S}~~>y),
+ (PreMonoidalFullSubcategory_bobj a x)~~{S}~~>(PreMonoidalFullSubcategory_bobj a y).
+ unfold hom; simpl; intros.
+ destruct a as [a apf].
+ destruct x as [x xpf].
+ destruct y as [y ypf].
+ simpl in *.
+ apply (a ⋊ f).
+ Defined.
+
+ Instance PreMonoidalFullSubcategory_first (a:S)
+ : Functor S S (fun x => PreMonoidalFullSubcategory_bobj x a) :=
+ { fmor := fun x y f => PreMonoidalFullSubcategory_first_fmor a f }.
+ unfold PreMonoidalFullSubcategory_first_fmor; intros; destruct a; destruct a0; destruct b; simpl in *.
+ apply (fmor_respects (-⋉x)); auto.
+ unfold PreMonoidalFullSubcategory_first_fmor; intros; destruct a; destruct a0; simpl in *.
+ apply (fmor_preserves_id (-⋉x)); auto.
+ unfold PreMonoidalFullSubcategory_first_fmor; intros;
+ destruct a; destruct a0; destruct b; destruct c; simpl in *.
+ apply (fmor_preserves_comp (-⋉x)); auto.
+ Defined.
+
+ Instance PreMonoidalFullSubcategory_second (a:S)
+ : Functor S S (fun x => PreMonoidalFullSubcategory_bobj a x) :=
+ { fmor := fun x y f => PreMonoidalFullSubcategory_second_fmor a f }.
+ unfold PreMonoidalFullSubcategory_second_fmor; intros; destruct a; destruct a0; destruct b; simpl in *.
+ apply (fmor_respects (x⋊-)); auto.
+ unfold PreMonoidalFullSubcategory_second_fmor; intros; destruct a; destruct a0; simpl in *.
+ apply (fmor_preserves_id (x⋊-)); auto.
+ unfold PreMonoidalFullSubcategory_second_fmor; intros;
+ destruct a; destruct a0; destruct b; destruct c; simpl in *.
+ apply (fmor_preserves_comp (x⋊-)); auto.
+ Defined.
+
+ Instance PreMonoidalFullSubcategory_is_Binoidal : BinoidalCat S PreMonoidalFullSubcategory_bobj :=
+ { bin_first := PreMonoidalFullSubcategory_first
+ ; bin_second := PreMonoidalFullSubcategory_second }.
+
+ Definition PreMonoidalFullSubcategory_assoc
+ : forall a b,
+ (PreMonoidalFullSubcategory_second a >>>> PreMonoidalFullSubcategory_first b) <~~~>
+ (PreMonoidalFullSubcategory_first b >>>> PreMonoidalFullSubcategory_second a).
+ Defined.
+
+ Definition PreMonoidalFullSubcategory_assoc_ll
+ : forall a b,
+ PreMonoidalFullSubcategory_second (a⊗b) <~~~>
+ PreMonoidalFullSubcategory_second b >>>> PreMonoidalFullSubcategory_second a.
+ intros.
+ Defined.
+
+ Definition PreMonoidalFullSubcategory_assoc_rr
+ : forall a b,
+ PreMonoidalFullSubcategory_first (a⊗b) <~~~>
+ PreMonoidalFullSubcategory_first a >>>> PreMonoidalFullSubcategory_first b.
+ intros.
+ Defined.
+
+ Definition PreMonoidalFullSubcategory_I := existT _ pmI Pobj_unit.
+
+ Definition PreMonoidalFullSubcategory_cancelr
+ : PreMonoidalFullSubcategory_first PreMonoidalFullSubcategory_I <~~~> functor_id _.
+ Defined.
+
+ Definition PreMonoidalFullSubcategory_cancell
+ : PreMonoidalFullSubcategory_second PreMonoidalFullSubcategory_I <~~~> functor_id _.
+ Defined.
+
+ Instance PreMonoidalFullSubcategory_PreMonoidal
+ : PreMonoidalCat PreMonoidalFullSubcategory_is_Binoidal PreMonoidalFullSubcategory_I :=
+ { pmon_assoc := PreMonoidalFullSubcategory_assoc
+ ; pmon_assoc_rr := PreMonoidalFullSubcategory_assoc_rr
+ ; pmon_assoc_ll := PreMonoidalFullSubcategory_assoc_ll
+ ; pmon_cancelr := PreMonoidalFullSubcategory_cancelr
+ ; pmon_cancell := PreMonoidalFullSubcategory_cancell
+ }.
+ Defined.
+End PreMonoidalFullSubcategory.
+*)
\ No newline at end of file