Proposition double_transformation_eq {C₁ C₂ : univalent_double_cat} {F G : lax_double_functor C₁ C₂} {τ θ : double_transformation F G} (p : ∏ (x : C₁), τ x = θ x) (pp : ∏ (x y : C₁) (f : x -->h y), double_transformation_hor_mor τ f = transportb_square (p x) (p y) (double_transformation_hor_mor θ f)) : τ = θ. Proof. use subtypePath. { intro. apply isapropunit. } use subtypePath. { intro. repeat (use isapropdirprod) ; apply isapropunit. } use subtypePath. { intro. use isapropdirprod ; [ apply isaprop_double_nat_trans_hor_id | ]. apply isaprop_double_nat_trans_hor_comp. } use total2_paths_b. - use nat_trans_eq. { apply homset_property. } exact p. - use eq_twosided_disp_nat_trans. intros x y f. refine (!_). etrans. { apply transportb_prebicat_twosided_disp_cat. } refine (_ @ !(pp x y f)). use transportb_disp_mor2_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.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.