equiv_empty_rec@{u} `{Funext} (A : Type@{u}) : Unit <~> ((Empty -> A) : Type@{u}) := (Build_Equiv@{Set u} _ _ (fun (_ : Unit) => @Empty_rec A) _). Global Instance istrunc_Empty@{} (n : trunc_index) : IsTrunc n.+1 Empty. Proof. refine (@istrunc_leq (-1) n.+1 tt _ _). apply istrunc_S. intros []. Defined.
Require Import Basics.Overture Basics.Equivalences Basics.Trunc.