Definition pathsdirprod_eta {X Y : UU} {x y : X × Y} (p : x = y) : p = pathsdirprod (maponpaths dirprod_pr1 p) (maponpaths dirprod_pr2 p). Proof. induction p. apply idpath. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics.