Definition funextsec2 X (Y:X->Type) (f g:∏ x,Y x) : (∏ x, f x = g x) -> f = g. Proof. intros e. exact (maponpaths (λ h x, interval_map (e x) h) interval_path). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.NullHomotopies. Require Import UniMath.MoreFoundations.Notations.