forall B : BAut (BAut Bool), (idpath B) = (idpath B). Proof. refine (center2_baut (BAut Bool) _). exists negb_center_baut_bool. apply center_baut_bool_central. 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.