+ Lemma TypesL_assoc_central a b c : CentralMorphism(H:=Types_binoidal) #((Types_assoc a b) c).
+ intros.
+ apply Build_CentralMorphism.
+ Opaque nd_id.
+ intros.
+ unfold bin_obj.
+ unfold ebc_bobj.
+ simpl.
+ unfold ehom.
+ nd_swap_ltac p pl_eqv.
+ setoid_rewrite p.
+ clear p.
+ setoid_rewrite (@nd_prod_split_left _ Rule pl_eqv _ _ _ []).
+ setoid_rewrite (@nd_prod_split_right _ Rule pl_eqv _ _ _ []).
+ repeat setoid_rewrite (@ndr_comp_associativity _ Rule pl_eqv).
+ setoid_rewrite <- (@ndr_comp_associativity _ Rule pl_eqv).
+
+ set (ni_commutes' (jud_mon_cancelr pl_eqv) g) as q.
+ Opaque nd_id.
+ simpl in q.
+ setoid_rewrite <- q.
+ clear q.
+
+ set (ni_commutes' (jud_mon_cancell pl_eqv) g) as q.
+ simpl in q.
+ set (coincide (pmon_triangle(PreMonoidalCat:=(Judgments_Category_premonoidal pl_eqv)))) as q'.
+ set (isos_forward_equal_then_backward_equal _ _ q') as qq.
+ simpl in qq.
+ setoid_rewrite qq in q.
+ clear q' qq.
+ setoid_rewrite <- q.
+
+ setoid_rewrite (@ndr_comp_associativity _ Rule pl_eqv).
+ apply ndr_comp_respects.
+ reflexivity.
+
+ Transparent nd_id.
+ apply (cndr_inert pl_cnd); auto.
+ apply ndpc_comp; auto.
+ apply ndpc_comp; auto.
+ apply ndpc_comp; auto.
+ apply ndpc_comp; auto.
+ apply ndpc_comp; auto.
+ apply ndpc_comp; auto.
+
+ Opaque nd_id.
+ intros.
+ unfold bin_obj.
+ unfold ebc_bobj.
+ simpl.
+ unfold ehom.
+ symmetry.
+ nd_swap_ltac p pl_eqv.
+ setoid_rewrite p.
+ clear p.
+ setoid_rewrite (@nd_prod_split_left _ Rule pl_eqv _ _ _ []).
+ setoid_rewrite (@nd_prod_split_right _ Rule pl_eqv _ _ _ []).
+ repeat setoid_rewrite (@ndr_comp_associativity _ Rule pl_eqv).
+ setoid_rewrite <- (@ndr_comp_associativity _ Rule pl_eqv).
+
+ set (ni_commutes' (jud_mon_cancelr pl_eqv) g) as q.
+ Opaque nd_id.
+ simpl in q.
+ setoid_rewrite <- q.
+ clear q.
+
+ set (ni_commutes' (jud_mon_cancell pl_eqv) g) as q.
+ simpl in q.
+ set (coincide (pmon_triangle(PreMonoidalCat:=(Judgments_Category_premonoidal pl_eqv)))) as q'.
+ set (isos_forward_equal_then_backward_equal _ _ q') as qq.
+ simpl in qq.
+ setoid_rewrite qq in q.
+ clear q' qq.
+ setoid_rewrite <- q.
+
+ setoid_rewrite (@ndr_comp_associativity _ Rule pl_eqv).
+ apply ndr_comp_respects.
+ reflexivity.
+
+ Transparent nd_id.
+ apply (cndr_inert pl_cnd); auto.
+ apply ndpc_comp; auto.
+ apply ndpc_comp; auto.
+ apply ndpc_comp; auto.
+ apply ndpc_comp; auto.
+ apply ndpc_comp; auto.
+ apply ndpc_comp; auto.
+ Qed.
+
+ Lemma TypesL_cancell_central a : CentralMorphism(H:=Types_binoidal) #(Types_cancell a).
+ intros.
+ apply Build_CentralMorphism.
+ Opaque nd_id.
+ intros.
+ unfold bin_obj.
+ unfold ebc_bobj.
+ simpl.
+ unfold ehom.
+ nd_swap_ltac p pl_eqv.
+ setoid_rewrite p.
+ clear p.
+ setoid_rewrite (@nd_prod_split_left _ Rule pl_eqv _ _ _ []).
+ setoid_rewrite (@nd_prod_split_right _ Rule pl_eqv _ _ _ []).
+ repeat setoid_rewrite (@ndr_comp_associativity _ Rule pl_eqv).
+ setoid_rewrite <- (@ndr_comp_associativity _ Rule pl_eqv).
+
+ set (ni_commutes' (jud_mon_cancelr pl_eqv) g) as q.
+ Opaque nd_id.
+ simpl in q.
+ setoid_rewrite <- q.
+ clear q.
+
+ set (ni_commutes' (jud_mon_cancell pl_eqv) g) as q.
+ simpl in q.
+ set (coincide (pmon_triangle(PreMonoidalCat:=(Judgments_Category_premonoidal pl_eqv)))) as q'.
+ set (isos_forward_equal_then_backward_equal _ _ q') as qq.
+ simpl in qq.
+ setoid_rewrite qq in q.
+ clear q' qq.
+ setoid_rewrite <- q.
+
+ setoid_rewrite (@ndr_comp_associativity _ Rule pl_eqv).
+ apply ndr_comp_respects.
+ reflexivity.
+
+ Transparent nd_id.
+ apply (cndr_inert pl_cnd); auto.
+ apply ndpc_comp; auto.
+ apply ndpc_comp; auto.
+ apply ndpc_comp; auto.
+ apply ndpc_comp; auto.
+ apply ndpc_comp; auto.
+ apply ndpc_comp; auto.
+
+ Opaque nd_id.
+ intros.
+ unfold bin_obj.
+ unfold ebc_bobj.
+ simpl.
+ unfold ehom.
+ symmetry.
+ nd_swap_ltac p pl_eqv.
+ setoid_rewrite p.
+ clear p.
+ setoid_rewrite (@nd_prod_split_left _ Rule pl_eqv _ _ _ []).
+ setoid_rewrite (@nd_prod_split_right _ Rule pl_eqv _ _ _ []).
+ repeat setoid_rewrite (@ndr_comp_associativity _ Rule pl_eqv).
+ setoid_rewrite <- (@ndr_comp_associativity _ Rule pl_eqv).
+
+ set (ni_commutes' (jud_mon_cancelr pl_eqv) g) as q.
+ Opaque nd_id.
+ simpl in q.
+ setoid_rewrite <- q.
+ clear q.
+
+ set (ni_commutes' (jud_mon_cancell pl_eqv) g) as q.
+ simpl in q.
+ set (coincide (pmon_triangle(PreMonoidalCat:=(Judgments_Category_premonoidal pl_eqv)))) as q'.
+ set (isos_forward_equal_then_backward_equal _ _ q') as qq.
+ simpl in qq.
+ setoid_rewrite qq in q.
+ clear q' qq.
+ setoid_rewrite <- q.
+
+ setoid_rewrite (@ndr_comp_associativity _ Rule pl_eqv).
+ apply ndr_comp_respects.
+ reflexivity.
+
+ Transparent nd_id.
+ apply (cndr_inert pl_cnd); auto.
+ apply ndpc_comp; auto.
+ apply ndpc_comp; auto.
+ apply ndpc_comp; auto.
+ apply ndpc_comp; auto.
+ apply ndpc_comp; auto.
+ apply ndpc_comp; auto.
+ Qed.
+
+ Lemma TypesL_cancelr_central a : CentralMorphism(H:=Types_binoidal) #(Types_cancelr a).
+ intros.
+ apply Build_CentralMorphism.
+ Opaque nd_id.
+ intros.
+ unfold bin_obj.
+ unfold ebc_bobj.
+ simpl.
+ unfold ehom.
+ nd_swap_ltac p pl_eqv.
+ setoid_rewrite p.
+ clear p.
+ setoid_rewrite (@nd_prod_split_left _ Rule pl_eqv _ _ _ []).
+ setoid_rewrite (@nd_prod_split_right _ Rule pl_eqv _ _ _ []).
+ repeat setoid_rewrite (@ndr_comp_associativity _ Rule pl_eqv).
+ setoid_rewrite <- (@ndr_comp_associativity _ Rule pl_eqv).
+
+ set (ni_commutes' (jud_mon_cancelr pl_eqv) g) as q.
+ Opaque nd_id.
+ simpl in q.
+ setoid_rewrite <- q.
+ clear q.
+
+ set (ni_commutes' (jud_mon_cancell pl_eqv) g) as q.
+ simpl in q.
+ set (coincide (pmon_triangle(PreMonoidalCat:=(Judgments_Category_premonoidal pl_eqv)))) as q'.
+ set (isos_forward_equal_then_backward_equal _ _ q') as qq.
+ simpl in qq.
+ setoid_rewrite qq in q.
+ clear q' qq.
+ setoid_rewrite <- q.
+
+ setoid_rewrite (@ndr_comp_associativity _ Rule pl_eqv).
+ apply ndr_comp_respects.
+ reflexivity.
+
+ Transparent nd_id.
+ apply (cndr_inert pl_cnd); auto.
+ apply ndpc_comp; auto.
+ apply ndpc_comp; auto.
+ apply ndpc_comp; auto.
+ apply ndpc_comp; auto.
+ apply ndpc_comp; auto.
+ apply ndpc_comp; auto.
+
+ Opaque nd_id.
+ intros.
+ unfold bin_obj.
+ unfold ebc_bobj.
+ simpl.
+ unfold ehom.
+ symmetry.
+ nd_swap_ltac p pl_eqv.
+ setoid_rewrite p.
+ clear p.
+ setoid_rewrite (@nd_prod_split_left _ Rule pl_eqv _ _ _ []).
+ setoid_rewrite (@nd_prod_split_right _ Rule pl_eqv _ _ _ []).
+ repeat setoid_rewrite (@ndr_comp_associativity _ Rule pl_eqv).
+ setoid_rewrite <- (@ndr_comp_associativity _ Rule pl_eqv).
+
+ set (ni_commutes' (jud_mon_cancelr pl_eqv) g) as q.
+ Opaque nd_id.
+ simpl in q.
+ setoid_rewrite <- q.
+ clear q.
+
+ set (ni_commutes' (jud_mon_cancell pl_eqv) g) as q.
+ simpl in q.
+ set (coincide (pmon_triangle(PreMonoidalCat:=(Judgments_Category_premonoidal pl_eqv)))) as q'.
+ set (isos_forward_equal_then_backward_equal _ _ q') as qq.
+ simpl in qq.
+ setoid_rewrite qq in q.
+ clear q' qq.
+ setoid_rewrite <- q.
+
+ setoid_rewrite (@ndr_comp_associativity _ Rule pl_eqv).
+ apply ndr_comp_respects.
+ reflexivity.
+
+ Transparent nd_id.
+ apply (cndr_inert pl_cnd); auto.
+ apply ndpc_comp; auto.
+ apply ndpc_comp; auto.
+ apply ndpc_comp; auto.
+ apply ndpc_comp; auto.
+ apply ndpc_comp; auto.
+ apply ndpc_comp; auto.
+ Qed.