+
+
+Section PreMonoidalSubCategory.
+
+ Context `(pm:PreMonoidalCat(I:=pmI)).
+ Context {Pobj}{Pmor}(S:SubCategory pm Pobj Pmor).
+ Context (Pobj_unit:Pobj pmI).
+ Context (Pobj_closed:forall {a}{b}, Pobj a -> Pobj b -> Pobj (a⊗b)).
+ Implicit Arguments Pobj_closed [[a][b]].
+ Context (Pmor_first: forall {a}{b}{c}{f}(pa:Pobj a)(pb:Pobj b)(pc:Pobj c)(pf:Pmor _ _ pa pb f),
+ Pmor _ _ (Pobj_closed pa pc) (Pobj_closed pb pc) (f ⋉ c)).
+ Context (Pmor_second: forall {a}{b}{c}{f}(pa:Pobj a)(pb:Pobj b)(pc:Pobj c)(pf:Pmor _ _ pa pb f),
+ Pmor _ _ (Pobj_closed pc pa) (Pobj_closed pc pb) (c ⋊ f)).
+ Context (Pmor_assoc: forall {a}{b}{c}(pa:Pobj a)(pb:Pobj b)(pc:Pobj c),
+ Pmor _ _
+ (Pobj_closed (Pobj_closed pa pb) pc)
+ (Pobj_closed pa (Pobj_closed pb pc))
+ #(pmon_assoc a c b)).
+ Context (Pmor_unassoc: forall {a}{b}{c}(pa:Pobj a)(pb:Pobj b)(pc:Pobj c),
+ Pmor _ _
+ (Pobj_closed pa (Pobj_closed pb pc))
+ (Pobj_closed (Pobj_closed pa pb) pc)
+ #(pmon_assoc a c b)⁻¹).
+ Context (Pmor_cancell: forall {a}(pa:Pobj a),
+ Pmor _ _ (Pobj_closed Pobj_unit pa) pa
+ #(pmon_cancell a)).
+ Context (Pmor_uncancell: forall {a}(pa:Pobj a),
+ Pmor _ _ pa (Pobj_closed Pobj_unit pa)
+ #(pmon_cancell a)⁻¹).
+ Context (Pmor_cancelr: forall {a}(pa:Pobj a),
+ Pmor _ _ (Pobj_closed pa Pobj_unit) pa
+ #(pmon_cancelr a)).
+ Context (Pmor_uncancelr: forall {a}(pa:Pobj a),
+ Pmor _ _ pa (Pobj_closed pa Pobj_unit)
+ #(pmon_cancelr a)⁻¹).
+ Implicit Arguments Pmor_first [[a][b][c][f]].
+ Implicit Arguments Pmor_second [[a][b][c][f]].
+
+ Definition PreMonoidalSubCategory_bobj (x y:S) :=
+ existT Pobj _ (Pobj_closed (projT2 x) (projT2 y)).
+
+ Definition PreMonoidalSubCategory_first_fmor (a:S) : forall {x}{y}(f:x~~{S}~~>y),
+ (PreMonoidalSubCategory_bobj x a)~~{S}~~>(PreMonoidalSubCategory_bobj y a).
+ unfold hom; simpl; intros.
+ destruct f.
+ destruct a as [a apf].
+ destruct x as [x xpf].
+ destruct y as [y ypf].
+ simpl in *.
+ exists (x0 ⋉ a).
+ apply Pmor_first; auto.
+ Defined.
+
+ Definition PreMonoidalSubCategory_second_fmor (a:S) : forall {x}{y}(f:x~~{S}~~>y),
+ (PreMonoidalSubCategory_bobj a x)~~{S}~~>(PreMonoidalSubCategory_bobj a y).
+ unfold hom; simpl; intros.
+ destruct f.
+ destruct a as [a apf].
+ destruct x as [x xpf].
+ destruct y as [y ypf].
+ simpl in *.
+ exists (a ⋊ x0).
+ apply Pmor_second; auto.
+ Defined.
+
+ Instance PreMonoidalSubCategory_first (a:S)
+ : Functor (S) (S) (fun x => PreMonoidalSubCategory_bobj x a) :=
+ { fmor := fun x y f => PreMonoidalSubCategory_first_fmor a f }.
+ unfold PreMonoidalSubCategory_first_fmor; intros; destruct a; destruct a0; destruct b; destruct f; destruct f'; simpl in *.
+ apply (fmor_respects (-⋉x)); auto.
+ unfold PreMonoidalSubCategory_first_fmor; intros; destruct a; destruct a0; simpl in *.
+ apply (fmor_preserves_id (-⋉x)); auto.
+ unfold PreMonoidalSubCategory_first_fmor; intros;
+ destruct a; destruct a0; destruct b; destruct c; destruct f; destruct g; simpl in *.
+ apply (fmor_preserves_comp (-⋉x)); auto.
+ Defined.
+
+ Instance PreMonoidalSubCategory_second (a:S)
+ : Functor (S) (S) (fun x => PreMonoidalSubCategory_bobj a x) :=
+ { fmor := fun x y f => PreMonoidalSubCategory_second_fmor a f }.
+ unfold PreMonoidalSubCategory_second_fmor; intros; destruct a; destruct a0; destruct b; destruct f; destruct f'; simpl in *.
+ apply (fmor_respects (x⋊-)); auto.
+ unfold PreMonoidalSubCategory_second_fmor; intros; destruct a; destruct a0; simpl in *.
+ apply (fmor_preserves_id (x⋊-)); auto.
+ unfold PreMonoidalSubCategory_second_fmor; intros;
+ destruct a; destruct a0; destruct b; destruct c; destruct f; destruct g; simpl in *.
+ apply (fmor_preserves_comp (x⋊-)); auto.
+ Defined.
+
+ Instance PreMonoidalSubCategory_is_Binoidal : BinoidalCat S PreMonoidalSubCategory_bobj :=
+ { bin_first := PreMonoidalSubCategory_first
+ ; bin_second := PreMonoidalSubCategory_second }.
+
+ Definition PreMonoidalSubCategory_assoc
+ : forall a b,
+ (PreMonoidalSubCategory_second a >>>> PreMonoidalSubCategory_first b) <~~~>
+ (PreMonoidalSubCategory_first b >>>> PreMonoidalSubCategory_second a).
+ admit.
+ Defined.
+
+ Definition PreMonoidalSubCategory_assoc_ll
+ : forall a b,
+ PreMonoidalSubCategory_second (a⊗b) <~~~>
+ PreMonoidalSubCategory_second b >>>> PreMonoidalSubCategory_second a.
+ intros.
+ admit.
+ Defined.
+
+ Definition PreMonoidalSubCategory_assoc_rr
+ : forall a b,
+ PreMonoidalSubCategory_first (a⊗b) <~~~>
+ PreMonoidalSubCategory_first a >>>> PreMonoidalSubCategory_first b.
+ intros.
+ admit.
+ Defined.
+
+ Definition PreMonoidalSubCategory_I := existT _ pmI (Pobj_unit).
+
+ Definition PreMonoidalSubCategory_cancelr : PreMonoidalSubCategory_first PreMonoidalSubCategory_I <~~~> functor_id _.
+ admit.
+ Defined.
+
+ Definition PreMonoidalSubCategory_cancell : PreMonoidalSubCategory_second PreMonoidalSubCategory_I <~~~> functor_id _.
+ admit.
+ Defined.
+
+ Instance PreMonoidalSubCategory_PreMonoidal : PreMonoidalCat PreMonoidalSubCategory_is_Binoidal PreMonoidalSubCategory_I :=
+ { pmon_assoc := PreMonoidalSubCategory_assoc
+ ; pmon_assoc_rr := PreMonoidalSubCategory_assoc_rr
+ ; pmon_assoc_ll := PreMonoidalSubCategory_assoc_ll
+ ; pmon_cancelr := PreMonoidalSubCategory_cancelr
+ ; pmon_cancell := PreMonoidalSubCategory_cancell
+ }.
+ admit.
+ admit.
+ admit.
+ admit.
+ admit.
+ admit.
+ admit.
+ Defined.
+
+End PreMonoidalSubCategory.