Definition homotsec_natural {X Y : UU} {f g : X → Y} (e : f ~ g) {x y : X} (p : x = y) : maponpaths f p @ e y = e x @ maponpaths g p. Proof. induction p. exact (!(pathscomp0rid _)). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics.