`{Funext} {A B : pType} : (A <~>* B) <~> (B <~>* A). 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.
Require Import Basics. Require Import Types. Require Import WildCat. Require Import Pointed.Core.