proposition: Proposition transportb_twosided_disp_cat_product {wx₁ wx₂ : category_binproduct C₁ C₂} {yz₁ yz₂ : category_binproduct C₃ C₄} {d₁ : twosided_disp_cat_product_data wx₁ yz₁} {d₂ : twosided_disp_cat_product_data wx₂ yz₂} {fg fg' : wx₁ --> wx₂} (p : fg = fg') {hk hk' : yz₁ --> yz₂} (q : hk = hk') (φ : d₁ -->[ fg' ][ hk' ] d₂) : transportb_disp_mor2 p q φ = transportb_disp_mor2 (maponpaths pr1 p) (maponpaths pr1 q) (pr1 φ) ,, transportb_disp_mor2 (maponpaths dirprod_pr2 p) (maponpaths dirprod_pr2 q) (pr2 φ).
proof: Proof. induction p, q ; cbn. apply idpath. Qed.
imports: UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.PrecategoryBinProduct UniMath.CategoryTheory.TwoSidedDisplayedCats.TwoSidedDispCat UniMath.CategoryTheory.TwoSidedDisplayedCats.Isos UniMath.CategoryTheory.TwoSidedDisplayedCats.Univalence