Z W Y : (Z ** W) ** Y = Z ** (W ** Y). Proof. refine (baut_bool_pairing_symm (Z ** W) Y @ _). refine (_ @ ap (fun X => Z ** X) (baut_bool_pairing_symm Y W)). apply path_baut, baut_bool_pairing_ZZ_Z_symm. 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.