proposition: Proposition lift_transportb {x y : E} {f g : x --> y} {τ₁ τ₂ : f ==> g} (p : τ₁ = τ₂) {xx : lift_disp_prebicat_data x} {yy : lift_disp_prebicat_data y} {ff : xx -->[ f ] yy} {gg : xx -->[ g ] yy} (ττ : ff ==>[ τ₂ ] gg) : transportb (λ (τ : f ==> g), ff ==>[ τ ] gg) p ττ = transportb (λ (τ : pr1 f ==> pr1 g), ff ==>[ τ ] gg) (maponpaths pr1 p) ττ.
proof: Proof. induction p. apply idpath. Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.DisplayedCats.Core UniMath.Bicategories.Core.Bicat UniMath.Bicategories.DisplayedBicats.DispBicat UniMath.Bicategories.Core.Univalence UniMath.Bicategories.DisplayedBicats.DispInvertibles UniMath.Bicategories.DisplayedBicats.DispAdjunctions UniMath.Bicategories.DisplayedBicats.DispUnivalence