proposition: Proposition equiv_pequiv_inverse `{Funext} {A B : pType} : (A <~>* B) <~> (B <~>* A).
proof: Proof. refine (issig_pequiv' _ _ oE _ oE (issig_pequiv' A B)^-1). srapply (equiv_functor_sigma' (equiv_equiv_inverse _ _)); intro e; cbn. exact (equiv_moveR_equiv_V _ _ oE equiv_path_inverse _ _). Defined.
imports: Basics Types WildCat Pointed.Core