Definition negb_weq_pair : @paths (∑ A : UU, A → bool) (bool ,, idfun bool) (bool ,, negb). Proof. refine ( total2_paths_f (B := λ A, A → bool) (s := bool ,, idfun bool) (s' := bool ,, negb) (weqtopaths negb_weq) _ ). refine (transportf_fun (idfun UU) (weqtopaths negb_weq) (idfun (idfun UU bool)) @ _). change (transportb (idfun UU) (weqtopaths negb_weq) = negb). refine (maponpaths _ (pathsinv0_weqtopaths _ ) @ _). apply weqpath_transport. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Univalence.