Type <~> Type. Proof. refine (((equiv_decidable_sum (fun X:Type => merely (X=A)))^-1) oE _ oE (equiv_decidable_sum (fun X:Type => merely (X=A)))). refine ((equiv_functor_sum_l (equiv_decidable_sum (fun X => merely (X.1=B)))^-1) oE _ oE (equiv_functor_sum_l (equiv_decidable_sum (fun X => merely (X.1=B))))). refine ((equiv_sum_assoc _ _ _) oE _ oE (equiv_sum_assoc _ _ _)^-1). apply equiv_functor_sum_r. assert (q : BAut B <~> {x : {x : Type & ~ merely (x = A)} & merely (x.1 = B)}). { refine (equiv_sigma_assoc _ _ oE _). apply equiv_functor_sigma_id; intros X. apply equiv_iff_hprop. - intros p. refine (fun q => _ ; p). strip_truncations. destruct q. exact (ne (equiv_path X B p)). - exact pr2. } refine (_ oE equiv_sum_symm _ _). apply equiv_functor_sum'. - exact (e^-1 oE q^-1). - exact (q oE e). Defined.
Require Import Basics Types. Require Import HoTT.Truncations. Require Import Universes.BAut Universes.Rigid. Require Import ExcludedMiddle.