`{f : A -> B} : ooPathSplit f -> IsEquiv f := fun ps => isequiv_pathsplit 0 (ps 2). Global Instance contr_oopathsplit_isequiv `(f : A -> B) `{IsEquiv _ _ f} : Contr (ooPathSplit f). Proof. apply contr_forall. Defined.
Require Import HoTT.Basics HoTT.Types.