fact: Definition cancelL_equiv {A B C} (g : B -> C) {f : A -> B} `{IsEquiv B C g} `{IsEquiv A C (g o f)} : A <~> B := Build_Equiv _ _ f (cancelL_isequiv g).
imports: Basics.Overture Basics.PathGroupoids Basics.Contractible Basics.Tactics