(e : Bool <~> Bool) : e == g (f e). Proof. unfold f, g; clear f g; intros []; simpl. - destruct (e true); reflexivity. - refine (eval_bool_isequiv e @ _). destruct (e true); reflexivity. Defined.
Require Import HoTT.Basics. Require Import Types.Equiv.