Definition transportb_dirprodeq' {X Y : UU} (Z : X × Y → UU) {x₁ x₂ : X} (p : x₁ = x₂) {y₁ y₂ : Y} (q : y₁ = y₂) (z : Z (x₂ ,, y₂)) : transportb (λ (w : X × Y), Z w) (dirprodeq _ _ (x₁ ,, y₁) (x₂ ,, y₂) p q) z = transportb (λ w, Z (w ,, _)) p (transportb (λ w, Z (_ ,, w)) q z). Proof. induction p, q. apply idpath. Defined.
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.