{A : Type} : Unit -> (A -> Unit) := fun _ _ => tt. Global Instance isequiv_unit_coind `{Funext} (A : Type) : IsEquiv (@ A) | 0. Proof. refine (isequiv_adjointify _ (fun f => tt) _ _). - intro f. apply path_forall; intros x; apply path_unit. - intro x; destruct x; reflexivity. Defined.
Require Import Basics.Overture Basics.Equivalences.