Definition make_para_sqr {a₁ a₂ b₁ b₂ : M} (v : a₁ --> a₂) (w : b₁ --> b₂) (f : para_mor a₁ b₁) (g : para_mor a₂ b₂) (φ : ob_of_para_mor f --> ob_of_para_mor g) (H : para_sqr_laws v w f g φ) : para_sqr v w f g := φ ,, H. Coercion mor_of_para_sqr {a₁ a₂ b₁ b₂ : M} {v : a₁ --> a₂} {w : b₁ --> b₂} {f : para_mor a₁ b₁} {g : para_mor a₂ b₂} (φ : para_sqr v w f g) : ob_of_para_mor f --> ob_of_para_mor g. Proof. exact (pr1 φ). 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.