Definition interval_path : left = right := squash_path true false.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.NullHomotopies. Require Import UniMath.MoreFoundations.Notations.