(g : BAut Bool <~> BAut Bool) (W : BAut Bool) : ap g (negb_center_baut_bool W) = negb_center_baut_bool (g W). Proof. revert g; equiv_intro equiv_baut_bool_aut_baut_bool Z. simpl. baut_reduce. refine (_ @ apD negb_center_baut_bool (baut_bool_pairing_1Z pt)^). rewrite transport_paths_lr, inv_V. apply moveL_pV. exact (concat_A1p baut_bool_pairing_1Z (negb_center_baut_bool pt)). Qed.
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.