{A B : Type} (f : A -> B) (postcomp := (fun (C : Type) (h : C -> A) => f o h)) (Aeq : IsEquiv (postcomp A)) (Beq : IsEquiv (postcomp B)) : IsEquiv f. Proof. set (g:=(postcomp B)^-1 idmap). pose proof (p:=eisretr (postcomp B) idmap : f o g = idmap). refine (isequiv_adjointify f g (ap10 p) (ap10 _)). apply (equiv_inj (postcomp A)). unfold postcomp; cbn. exact (ap (fun k => k o f) p). Defined.
Require Import