`{Funext} (O : ReflectiveSubuniverse) (P Q : pType) `{In O Q} : ([O P, _] ->** Q) <~>* (P ->** Q). Proof. snrapply Build_pEquiv. - exact (Build_pMap _ _ (fun f => f o* pto O P) 1). - transparent assert (e : (([O P, _] ->* Q) <~> (P ->* Q))). + refine (issig_pmap P Q oE _ oE (issig_pmap [O P, _] Q)^-1%equiv). snrapply equiv_functor_sigma'. * rapply equiv_o_to_O. * intro f; cbn. apply (equiv_concat_l 1). + apply (equiv_isequiv e). Defined.
Require Import Basics Types ReflectiveSubuniverse Pointed.Core.