Definition negb_weq : bool ≃ bool. Proof. exists negb. cbv. intros. use tpair. - use tpair. + exact (negb y). + induction y; apply idpath. - cbn. intro t. induction t as [b eq]. induction b; induction eq; apply idpath. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Univalence.