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