`{O : ReflectiveSubuniverse} {X Y : pType@{u}} : O_pcover O (X * Y) pt <~>* [(O_pcover O X pt) * (O_pcover O Y pt), _]. Proof. srapply Build_pEquiv'. { refine (_ oE equiv_functor_sigma_id _). 2: intro; nrapply equiv_path_O_prod. nrapply equiv_sigma_prod_prod. } nrapply path_prod; cbn. all: snrapply path_sigma'. 1,3: exact idpath. all: cbn. all: by rewrite concat_p1, concat_Vp. Defined.
Require Import Basics Types HFiber Truncations.Core Truncations.SeparatedTrunc Pointed