negb_center2_baut_baut_bool <> (fun Z => idpath (idpath Z)). Proof. intros oops. exact (nontrivial_negb_center_baut_bool (((ap (center2_baut (BAut Bool)))^-1 (oops @ (id_center2_baut (BAut Bool))^))..1)). 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.