proposition: Proposition transportbf_disp_mor2 {D : twosided_disp_cat_data} {x₁ x₂ : C₁} {y₁ y₂ : C₂} {xy₁ : D x₁ y₁} {xy₂ : D x₂ y₂} {f₁ f₂ : x₁ --> x₂} (p : f₁ = f₂) {g₁ g₂ : y₁ --> y₂} (q : g₁ = g₂) (fg : xy₁ -->[ f₁ ][ g₁ ] xy₂) : transportb_disp_mor2 p q (transportf_disp_mor2 p q fg) = fg.
proof: Proof. induction p, q ; cbn. apply idpath. Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.PrecategoryBinProduct