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