Definition make_prod_square {D₁ D₂ : univalent_double_cat} {x₁ x₂ y₁ y₂ : D₁} {v₁ : x₁ -->v y₁} {v₂ : x₂ -->v y₂} {h₁ : x₁ -->h x₂} {h₂ : y₁ -->h y₂} (s : square v₁ v₂ h₁ h₂) {x₁' x₂' y₁' y₂' : D₂} {v₁' : x₁' -->v y₁'} {v₂' : x₂' -->v y₂'} {h₁' : x₁' -->h x₂'} {h₂' : y₁' -->h y₂'} (s' : square v₁' v₂' h₁' h₂') : square (make_prod_ver v₁ v₁') (make_prod_ver v₂ v₂') (make_prod_hor h₁ h₁') (make_prod_hor h₂ h₂') := s ,, s'.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.TwoSidedDispCat. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Isos. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Univalence. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.DisplayedFunctor. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.DisplayedNatTrans. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Examples.ProdOfTwosidedDispCat. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.Core.Examples.BicatOfUnivCats. Require Import UniMath.Bicategories.Limits.Products. Require Import UniMath.Bicategories.DoubleCategories.Basics.DoubleCategoryBasics. Require Import UniMath.Bicategories.DoubleCategories.Core.DoubleCats. Require Import UniMath.Bicategories.DoubleCategories.Core.UnivalentDoubleCats. Require Import UniMath.Bicategories.DoubleCategories.Core.DoubleFunctor.Basics. Require Import UniMath.Bicategories.DoubleCategories.Core.DoubleTransformation. Require Import UniMath.Bicategories.DoubleCategories.Core.BicatOfDoubleCats. Require Import UniMath.Bicategories.DoubleCategories.Core.InvertiblesAndEquivalences. Require Import UniMath.Bicategories.DoubleCategories.DerivedLaws.TransportLaws. Require Import UniMath.Bicategories.DoubleCategories.DerivedLaws.Variations.