Definition strict_double_cat_laws {C : category} {D : twosided_disp_cat C C} (I : hor_id D) (Cm : hor_comp D) : UU := ∑ (lp : strict_double_cat_id_left I Cm) (rp : strict_double_cat_id_right I Cm) (ap : strict_double_cat_assoc Cm), strict_double_cat_id_left_square lp × strict_double_cat_id_right_square rp × strict_double_cat_assoc_square ap.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Core.Setcategories. Require Import UniMath.CategoryTheory.Categories.CategoryOfSetCategories. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.TwoSidedDispCat. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.DisplayedFunctor. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.DisplayedNatTrans. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Isos. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Univalence. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Strictness. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.TransportLaws. Require Import UniMath.Bicategories.DoubleCategories.Basics.DoubleCategoryBasics.