- { 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.
+ { pmon_assoc := PreMonoidalFullSubcategory_assoc
+ ; pmon_assoc_rr := PreMonoidalFullSubcategory_assoc_rr
+ ; pmon_assoc_ll := PreMonoidalFullSubcategory_assoc_ll
+ ; pmon_cancelr := PreMonoidalFullSubcategory_cancelr
+ ; pmon_cancell := PreMonoidalFullSubcategory_cancell
+ }.
+ apply Build_Pentagon.
+ intros.
+ destruct a as [a apf].
+ destruct b as [b bpf].
+ destruct c as [c cpf].
+ destruct d as [d dpf].
+ simpl.
+ apply (pmon_pentagon(PreMonoidalCat:=pm)).
+
+ apply Build_Triangle.
+ intros.
+ destruct a as [a apf].
+ destruct b as [b bpf].
+ simpl.
+ apply (pmon_triangle(PreMonoidalCat:=pm)).
+ simpl.
+ apply (pmon_triangle(PreMonoidalCat:=pm)).
+
+ intros.
+ destruct a as [a apf].
+ destruct c as [c cpf].
+ destruct d as [d dpf].
+ simpl.
+ apply (pmon_coherent_r(PreMonoidalCat:=pm)).
+
+ intros.
+ destruct a as [a apf].
+ destruct c as [c cpf].
+ destruct d as [d dpf].
+ simpl.
+ apply (pmon_coherent_l(PreMonoidalCat:=pm)).
+
+ intros.
+ destruct a as [a apf].
+ destruct b as [b bpf].
+ destruct c as [c cpf].
+ simpl.
+ apply central_full.
+ simpl.
+ apply (pmon_assoc_central(PreMonoidalCat:=pm)).
+
+ intros.
+ destruct a as [a apf].
+ simpl.
+ apply central_full.
+ simpl.
+ apply (pmon_cancelr_central(PreMonoidalCat:=pm)).
+
+ intros.
+ destruct a as [a apf].
+ simpl.
+ apply central_full.
+ simpl.
+ apply (pmon_cancell_central(PreMonoidalCat:=pm)).
+ Defined.
+