Y Z W : Y ** (Z ** W) -> Z ** (Y ** W). Proof. intros e. simple refine (equiv_adjointify (baut_bool_pairing_ZZ_Z_symm_part1 e) _ _ _). - intros f. exact (baut_bool_pairing_ZZ_Z_symm_lemma e f (merely_inhab_baut_bool Y)). - intros f. apply path_equiv, path_arrow; intros y. change ((e y) (baut_bool_pairing_ZZ_Z_symm_lemma e f (merely_inhab_baut_bool Y)) = f y). refine (ap (e y o baut_bool_pairing_ZZ_Z_symm_lemma e f) (path_ishprop _ (tr y)) @ _). simpl. apply eisretr. - intros z. assert (IsHSet Z) by exact _. refine (Trunc_rec _ (merely_inhab_baut_bool Y)); intros y. refine (ap (baut_bool_pairing_ZZ_Z_symm_lemma e _) (path_ishprop _ (tr y)) @ _). simpl. refine (eissect _ _). 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.