Definition paths_pathsdirprod {X Y : UU} {x₁ x₂ : X} {y₁ y₂ : Y} {p₁ p₂ : x₁ = x₂} {q₁ q₂ : y₁ = y₂} (r₁ : p₁ = p₂) (r₂ : q₁ = q₂) : pathsdirprod p₁ q₁ = pathsdirprod p₂ q₂. Proof. induction r₁, r₂. apply idpath. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics.