Definition para_mor_associator {w x y z : M} (f : para_mor w x) (g : para_mor x y) (h : para_mor y z) : para_sqr (identity _) (identity _) (comp_para_mor f (comp_para_mor g h)) (comp_para_mor (comp_para_mor f g) h). Proof. use make_para_sqr. - apply mon_lassociator. - abstract (unfold para_sqr_laws ; cbn ; rewrite id_right ; rewrite !tensor_comp_l_id_l ; rewrite !assoc ; rewrite <- mon_lassociator_lassociator ; rewrite !assoc' ; apply maponpaths ; rewrite !assoc ; rewrite <- tensor_lassociator ; rewrite tensor_id_id ; apply idpath). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Core.Setcategories. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Univalence. Require Import UniMath.CategoryTheory.DisplayedCats.Constructions. Require Import UniMath.CategoryTheory.DisplayedCats.Univalence. Require Import UniMath.CategoryTheory.DisplayedCats.Projection. Require Import UniMath.CategoryTheory.Monoidal.Categories. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.TwoSidedDispCat. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Isos. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Strictness. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Discrete. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Univalence. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Total. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Examples.Constant. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Examples.DispCatOnTwoSidedDispCat. Import MonoidalNotations.