Proposition transportb_disp_mor2_two_cat_arrow {x₁ x₂ y₁ y₂ : C} {f f' : x₁ --> x₂} (p : f' = f) {g g' : y₁ --> y₂} (q : g' = g) {h₁ : two_cat_arrow_twosided_disp_cat_data x₁ y₁} {h₂ : two_cat_arrow_twosided_disp_cat_data x₂ y₂} (τ : h₁ -->[ f ][ g ] h₂) : transportb_disp_mor2 p q τ = (_ ◃ idto2mor q) • τ • (idto2mor (!p) ▹ _). Proof. induction p, q. cbn. rewrite lwhisker_id2. rewrite id2_rwhisker. rewrite id2_left. rewrite id2_right. apply idpath. Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Core.TwoCategories. Import TwoCategories.Notations. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.TwoSidedDispCat. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Isos. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Univalence. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Total. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Strictness. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Discrete.