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