Proposition lax_double_functor_transportf_square {C₁ C₂ : univalent_double_cat} (F : lax_double_functor C₁ C₂) {x₁ x₂ y₁ y₂ : C₁} {v₁ v₂ : x₁ -->v y₁} (p : v₁ = v₂) {w₁ w₂ : x₂ -->v y₂} (q : w₁ = w₂) {h : x₁ -->h x₂} {k : y₁ -->h y₂} (s : square v₁ w₁ h k) : #s F (transportf_square p q s) = transportf_square (maponpaths (λ z, #v F z) p) (maponpaths (λ z, #v F z) q) (#s F s). Proof. induction p, q. cbn. apply idpath. Qed.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.TwoSidedDispCat. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Univalence. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.DoubleCategories.Core.DoubleCats. Require Import UniMath.Bicategories.DoubleCategories.Core.UnivalentDoubleCats.