(f : Bool -> Bool) `{IsEquiv Bool Bool f} : f false = negb (f true). Proof. pose proof (eissect f true). pose proof (eissect f false). simpl in *. destruct (f true), (f false). - etransitivity; try (eassumption || (symmetry; eassumption)). - simpl. reflexivity. - simpl. reflexivity. - etransitivity; try (eassumption || (symmetry; eassumption)). Defined.
Require Import HoTT.Basics. Require Import Types.Equiv.