negb_center_baut_bool <> (fun Z => idpath Z). Proof. intros oops. pose (p := ap10_equiv ((ap (center_baut Bool))^-1 (oops @ (id_center_baut Bool)^))..1 true). exact (false_ne_true p). 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.