Proposition pair_double_transformation_hor_comp : double_nat_trans_hor_comp pair_double_transformation_twosided_disp_nat_trans (lax_double_functor_hor_comp F) (lax_double_functor_hor_comp G). Proof. use (make_double_nat_trans_hor_comp (F := F) (G := G)). cbn -[prod_univalent_double_cat bicat_of_double_cats]. intros x y z h k. refine (_ @ !(transportb_prod_double_cat _ _ _ _ _)). use dirprodeq ; cbn -[prod_univalent_double_cat bicat_of_double_cats]. - refine (_ @ double_transformation_comp_h τ h k @ _). + refine (maponpaths (λ z, z ⋆v _) _). refine (!_). cbn. etrans. { apply maponpaths. apply (square_id_left_v (C := D₁)). } unfold transportb_square. etrans. { apply (transportf_f_square (C := D₁)). } apply transportf_square_id. + use transportb_square_eq. refine (maponpaths (λ z, _ ⋆v z) _). cbn. etrans. { apply maponpaths. apply (square_id_left_v (C := D₁)). } unfold transportb_square. etrans. { apply (transportf_f_square (C := D₁)). } apply transportf_square_id. - refine (_ @ double_transformation_comp_h θ h k @ _). + refine (maponpaths (λ z, z ⋆v _) _). refine (!_). cbn. etrans. { apply maponpaths. apply (square_id_left_v (C := D₂)). } unfold transportb_square. etrans. { apply (transportf_f_square (C := D₂)). } apply transportf_square_id. + use transportb_square_eq. refine (maponpaths (λ z, _ ⋆v z) _). cbn. etrans. { apply maponpaths. apply (square_id_left_v (C := D₂)). } unfold transportb_square. etrans. { apply (transportf_f_square (C := D₂)). } apply transportf_square_id. 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.