Definition comp_para_sqr {x₁ x₂ y₁ y₂ z₁ z₂ : M} {v₁ : x₁ --> x₂} {v₂ : y₁ --> y₂} {v₃ : z₁ --> z₂} {f₁ : para_mor x₁ y₁} {f₂ : para_mor y₁ z₁} {g₁ : para_mor x₂ y₂} {g₂ : para_mor y₂ z₂} (φ : para_sqr v₁ v₂ f₁ g₁) (ψ : para_sqr v₂ v₃ f₂ g₂) : para_sqr v₁ v₃ (comp_para_mor f₁ f₂) (comp_para_mor g₁ g₂). Proof. use make_para_sqr. - exact (ψ #⊗ φ). - abstract (unfold para_sqr_laws ; cbn ; rewrite !assoc ; rewrite tensor_lassociator ; rewrite !assoc' ; apply maponpaths ; rewrite !assoc ; rewrite <- tensor_comp_mor ; rewrite eq_of_para_sqr ; rewrite id_right ; rewrite tensor_comp_l_id_l ; rewrite !assoc' ; rewrite eq_of_para_sqr ; 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.