fact: Definition equiv_ap_inv `(f : A -> B) `{IsEquiv A B f} (x y : B) : (f^-1 x = f^-1 y) <~> (x = y) := (@equiv_ap B A f^-1 _ x y)^-1%equiv.
imports: Basics.Overture Basics.PathGroupoids Basics.Contractible Basics.Tactics