(Z : BAut Bool) : Z <~> Z := equiv_path Z Z (negb_center_baut_bool Z).
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.