Definition twosided_disp_functor_double_cat_laws {C₁ C₂ : univalent_double_cat} {F : C₁ ⟶ C₂} (FF : twosided_disp_functor_double_cat_data C₁ C₂ F) : UU := (∏ (x y : C₁) (h : x -->h y), twosided_disp_functor_double_cat_data_square FF (id_v_square h) = transportb_square (functor_id _ _) (functor_id _ _) (id_v_square (FF _ _ h))) × (∏ (x₁ x₂ x₃ y₁ y₂ y₃ : C₁) (h₁ : x₁ -->h y₁) (h₂ : x₂ -->h y₂) (h₃ : x₃ -->h y₃) (vx₁ : x₁ -->v x₂) (vy₁ : y₁ -->v y₂) (s₁ : square vx₁ vy₁ h₁ h₂) (vx₂ : x₂ -->v x₃) (vy₂ : y₂ -->v y₃) (s₂ : square vx₂ vy₂ h₂ h₃), twosided_disp_functor_double_cat_data_square FF (s₁ ⋆v s₂) = transportb_square (functor_comp _ _ _) (functor_comp _ _ _) (twosided_disp_functor_double_cat_data_square FF s₁ ⋆v twosided_disp_functor_double_cat_data_square FF 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.DisplayedFunctor. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.DisplayedNatTrans. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Isos. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Univalence. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.Core.Invertible_2cells. Require Import UniMath.Bicategories.DisplayedBicats.DispBicat. Import DispBicat.Notations. Require Import UniMath.Bicategories.DisplayedBicats.DispUnivalence. Require Import UniMath.Bicategories.DisplayedBicats.Examples.DispBicatOfDispCats. Require Import UniMath.Bicategories.DisplayedBicats.Examples.DispBicatOfTwoSidedDispCat. Require Import UniMath.Bicategories.DisplayedBicats.Examples.DisplayedCatToBicat. Require Import UniMath.Bicategories.DisplayedBicats.Examples.FullSub. Require Import UniMath.Bicategories.DisplayedBicats.Examples.Prod. Require Import UniMath.Bicategories.Core.Examples.BicatOfUnivCats. Require Import UniMath.Bicategories.DoubleCategories.Basics.DoubleCategoryBasics. Require Import UniMath.Bicategories.DoubleCategories.Core.DoubleFunctor. Require Import UniMath.Bicategories.DoubleCategories.Core.DoubleTransformation. Require Import UniMath.Bicategories.DoubleCategories.Core.BicatOfDoubleCats. Require Import UniMath.Bicategories.DoubleCategories.Core.DoubleCats.