Proposition pair_lax_double_functor_pr2_hor_comp : double_nat_trans_hor_comp pair_lax_double_functor_pr2_twosided_disp_nat_trans (lax_double_functor_hor_comp (pair_lax_double_functor · prod_univalent_double_cat_pr2 D₁ D₂)) (lax_double_functor_hor_comp G). Proof. use (make_double_nat_trans_hor_comp (F := pair_lax_double_functor · prod_univalent_double_cat_pr2 D₁ D₂)). intros x y z h k ; cbn ; unfold bindelta_pair_pr1_data ; cbn. etrans. { apply (square_id_right_v (C := D₂)). } unfold transportb_square. etrans. { exact (transportf_f_square _ _ _ _ _). } etrans. { apply maponpaths. apply (square_id_left_v (C := D₂)). } refine (!_). etrans. { apply maponpaths. etrans. { apply maponpaths_2. apply (comp_h_square_id (C := D₂)). } apply (square_id_left_v (C := D₂)). } unfold transportb_square. etrans. { exact (transportf_f_square _ _ _ _ _). } rewrite !transportf_f_square. use transportf_square_eq. apply idpath. Qed.
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.