Definition total2_paths_2_b {X Y : UU} (Z : X → Y → UU) {x₁ x₂ : X} (p : x₁ = x₂) {y₁ y₂ : Y} (q : y₁ = y₂) {z₁ : Z x₁ y₁} {z₂ : Z x₂ y₂} (r : z₁ = transportb (λ w, Z w _) p (transportb (λ w, Z _ w) q z₂)) : (x₁ ,, y₁ ,, z₁ : ∑ (x : X) (y : Y), Z x y) = (x₂ ,, y₂ ,, z₂ : ∑ (x : X) (y : Y), Z x y). Proof. induction p, q ; cbn in *. induction r. 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.