Definition twosided_prod_transportb_alt {D : twosided_disp_cat} {x₁ x₂ : C₁} {y₁ y₂ : C₂} {xy₁ : D x₁ y₁} {xy₂ : D x₂ y₂} {f₁ f₂ : x₁ --> x₂} {g₁ g₂ : y₁ --> y₂} (fg : xy₁ -->[ f₁ ][ g₁ ] xy₂) (p : f₂ = f₁) (q : g₂ = g₁) : transportb (λ z, _ -->[ _ ][ z ] _) q (transportb (λ z, _ -->[ z ][ _ ] _) p fg) = transportb (λ z, _ -->[ pr1 z ][ pr2 z ] _) (pathsdirprod p q) fg.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.PrecategoryBinProduct.