forall (Z:BAut Bool), Z = Z. Proof. apply center_baut; try exact _. exists equiv_negb. intros g; apply abelian_aut_bool. 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.