Lemma maponpaths_for_constant_function {T1 T2 : UU} (x : T2) {t1 t2 : T1} (e: t1 = t2): maponpaths (fun _: T1 => x) e = idpath x. Proof. induction e. apply idpath. Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics.