fact: Definition isequiv_isequiv_precompose {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.
imports: Basics.Overture Basics.PathGroupoids Basics.Contractible Basics.Tactics