`{Funext} (O : ReflectiveSubuniverse) (X : pType) `{IsConnected O X} (Y : pType) `{In O Y} : Contr (X ->* Y). Proof. srapply (contr_equiv' ([O X, _] ->* Y)). rapply pequiv_o_pto_O. Defined.
Require Import Basics Types WildCat Truncations