Y Z W : Y ** (Z ** W) <~> Z ** (Y ** W). Proof. refine (equiv_adjointify (baut_bool_pairing_ZZ_Z_symm_map Y Z W) (baut_bool_pairing_ZZ_Z_symm_map Z Y W) (baut_bool_pairing_ZZ_Z_symm_inv Y Z W) (baut_bool_pairing_ZZ_Z_symm_inv Z Y W)). 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.