fact: Definition Book_4_2_2 := fun (A B : Type) (f : A -> B) (feq : IsEquiv f) (y : B) => @HoTT.Basics.Overture.eisadj B A f^-1 (@HoTT.Basics.Equivalences.isequiv_inverse A B f feq) y.
imports: HoTT(Basics Truncations)