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