X : X * Unit <~> X. Proof. refine (Build_Equiv _ _ fst _). simple refine (Build_IsEquiv _ _ _ (fun x => (x,tt)) _ _ _). - intros x; reflexivity. - intros [x []]; reflexivity. - intros [x []]; reflexivity. Defined.
Require Import Basics.Overture Basics.Equivalences Basics.PathGroupoids Require Import Types.Empty.