Definition interval_map {Y} {y y':Y} : y = y' -> interval -> Y. Proof. intros e. set (f := λ t:bool, if t then y else y'). refine (cone_squash_map f (f false) _). intros v. induction v. { exact e. } { reflexivity. } Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.NullHomotopies. Require Import UniMath.MoreFoundations.Notations.