Proposition pair_double_transformation_unique : isaprop (∑ (γ : F ==> G), (γ ▹ prod_univalent_double_cat_pr1 D₁ D₂ = τ) × (γ ▹ prod_univalent_double_cat_pr2 D₁ D₂ = θ)). Proof. use invproofirrelevance. intros γ₁ γ₂. use subtypePath. { intro. apply isapropdirprod ; apply cellset_property. } induction γ₁ as [ γ₁ [ p₁ q₁ ]]. induction γ₂ as [ γ₂ [ p₂ q₂ ]]. cbn. pose (p := p₁ @ !p₂). pose (q := q₁ @ !q₂). use double_transformation_eq. - intro x. use dirprodeq. + exact (double_transformation_eq_ob p x). + exact (double_transformation_eq_ob q x). - intros x y h. refine (_ @ !(transportb_prod_double_cat _ _ _ _ _)). use dirprodeq. + refine (double_transformation_eq_hor_mor p h @ _). use transportb_square_eq. apply idpath. + refine (double_transformation_eq_hor_mor q h @ _). use transportb_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.