(e : BAut Bool <~> BAut Bool) (Z W : BAut Bool) : (e^-1 Z ** W) = (Z ** e W). Proof. apply path_baut; simpl. refine ((equiv_equiv_path _ _) oE _ oE (equiv_equiv_path _ _)^-1). refine (_ oE (@equiv_moveL_equiv_M _ _ e _ W Z) oE _). - apply equiv_inverse, equiv_path_sigma_hprop. - apply equiv_path_sigma_hprop. 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.