`{Funext} : Bool <~> (Bool <~> Bool). Proof. refine (equiv_adjointify g f _ _). - intro e. apply path_equiv, path_forall. intros b; symmetry; apply aut_bool_canonical. - intros []; reflexivity. Defined.
Require Import HoTT.Basics. Require Import Types.Equiv.