{Y Z W} (e : Y ** (Z ** W)) (z : Z) : Y ** W. Proof. simple refine (equiv_adjointify _ _ _ _). + exact (fun y => e y z). + intros w. destruct (path_baut_bool_inhab W w). destruct (path_baut_bool_inhab Z z). destruct (dec (z=w)). * exact (e^-1 (equiv_idmap _)). * exact (e^-1 equiv_negb). + intros w. destruct (path_baut_bool_inhab W w). destruct (path_baut_bool_inhab Z z). simpl. destruct z,w; simpl; refine (ap10_equiv (eisretr e _) _). + intros y. destruct (path_baut_bool_inhab Y y). destruct (path_baut_bool_inhab Z z). destruct (path_baut_bool_inhab W (e y z)). simpl. case (dec (z = e y z)); intros p; apply moveR_equiv_V; destruct (aut_bool_idmap_or_negb (e y)) as [q|q]. * symmetry; assumption. * case (not_fixed_negb z (p @ ap10_equiv q z)^). * case (p (ap10_equiv q z)^). * symmetry; assumption. 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.