fact: Definition equiv_empty_rec@{u} `{Funext} (A : Type@{u}) : Unit <~> ((Empty -> A) : Type@{u}) := (Build_Equiv@{Set u} _ _ (fun (_ : Unit) => @Empty_rec A) _).
imports: Basics.Overture Basics.Equivalences Basics.Trunc