{Y Z W} (e : Y ** (Z ** W)) (f : Y ** W) : merely Y -> Z. Proof. pose (k := (fun y => (e y)^-1 (f y))). refine (merely_rec_hset k); intros y1 y2. destruct (path_baut_bool_inhab Y y1). destruct (path_baut_bool_inhab W (f y1)). destruct (path_baut_bool_inhab Z (k y1)). destruct (aut_bool_idmap_or_negb f) as [p|p]; refine (ap (e y1)^-1 (ap10_equiv p y1) @ _); refine (_ @ (ap (e y2)^-1 (ap10_equiv p y2))^); clear p f k; simpl. + destruct (dec (y1=y2)) as [p|p]. { exact (ap (fun y => (e y)^-1 y) p). } destruct (aut_bool_idmap_or_negb (e y1)) as [q1|q1]; destruct (aut_bool_idmap_or_negb (e y2)) as [q2|q2]. * case (p ((ap e)^-1 (q1 @ q2^))). * rewrite q1, q2. exact (negb_ne p). * rewrite q1, q2. symmetry. exact (negb_ne (fun r => p r^)). * case (p ((ap e)^-1 (q1 @ q2^))). + destruct (dec (y1=y2)) as [p|p]. { exact (ap (fun y => (e y)^-1 (negb y)) p). } destruct (aut_bool_idmap_or_negb (e y1)) as [q1|q1]; destruct (aut_bool_idmap_or_negb (e y2)) as [q2|q2]. * case (p ((ap e)^-1 (q1 @ q2^))). * rewrite q1, q2. exact (negb_ne (fun r => p ((ap negb)^-1 r))). * rewrite q1, q2. symmetry. exact (negb_ne (fun r => p ((ap negb)^-1 r)^)). * case (p ((ap e)^-1 (q1 @ q2^))). 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.