`{Funext} {A B C : pType} (f : B <~>* C) : (A ->** B) <~>* (A ->** C). Proof. srapply Build_pEquiv'. - exact (equiv_postcompose_cat_equiv f). - cbn; unfold "o*", point_pforall; cbn. by pelim f. Defined.
Require Import Basics. Require Import Types. Require Import WildCat. Require Import Pointed.Core.