BAut Bool -> BAut Bool -> BAut Bool. Proof. intros Z W. exists (Z <~> W). baut_reduce; simpl. apply tr, symmetry. exact (path_universe equiv_bool_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.