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