`{Funext} {A B C : pType} (f : A <~>* B) : (B ->** C) <~>* (A ->** C). Proof. srapply Build_pEquiv'. - exact (equiv_precompose_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.