negb_baut_bool pt = equiv_negb. Proof. pose (c := aut_bool_idmap_or_negb (negb_baut_bool pt)). destruct c. - pose (negb_baut_bool_ne_idmap pt p). contradiction. - assumption. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import Constant. Require Import HoTT.Truncations.Core HoTT.Truncations.Connectedness. Require Import Universes.BAut. Require Import Pointed.Core.