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 (pr1 w) (pr2 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.