`(O : ReflectiveSubuniverse) {X Y : pType} (f : X ->* Y) : O_pfunctor O f o* pto O X ==* pto O Y o* f. Proof. nrapply pO_rec_beta. Defined.
Require Import Basics Types ReflectiveSubuniverse Pointed.Core.