Proposition transportfb_square' {C : double_cat} {x₁ x₂ y₁ y₂ : C} {v₁ v₁' : x₁ -->v y₁} {v₂ v₂' : x₂ -->v y₂} {h₁ : x₁ -->h x₂} {h₂ : y₁ -->h y₂} (p p' : v₁ = v₁') (q q' : v₂ = v₂') (s : square v₁' v₂' h₁ h₂) : transportf_square p q (transportb_square p' q' s) = s. Proof. induction p, q. assert (p' = idpath _) as r by apply isaset_ver_mor. rewrite r ; clear r. assert (q' = idpath _) as r by apply isaset_ver_mor. rewrite r ; clear r. 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.TwoSidedDisplayedCats.TwoSidedDispCat. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Isos. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Univalence. Require Import UniMath.Bicategories.Core.Examples.BicatOfUnivCats. Require Import UniMath.Bicategories.DoubleCategories.Basics.DoubleCategoryBasics.