Definition underlyingLoop {X:PointedType} (l:loopSpace X) : basepoint X = basepoint X. Proof. intros. exact l. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics.