fact: Definition pequiv_adjointify {A B : pType} (f : A ->* B) (f' : B ->* A) (r : f o* f' ==* pmap_idmap) (s : f' o* f == pmap_idmap) : A <~>* B := (Build_pEquiv _ _ f (isequiv_adjointify f f' r s)).
imports: Basics Types WildCat Pointed.Core