Definition PathOverConstant_map2_apd {X:Type} {x x':X} {p:x=x'} {Z : Type} {f : X -> Z} : PathOverConstant_map2 (apd f p) = maponpaths f p. Proof. now induction p. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.PartA.