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. induction p, q ; cbn. apply idpath. Qed.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.TwoSidedDispCat. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Isos. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Univalence.