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