fact: Definition equiv_cancelL {A} {x y z : A} (p : x = y) (q r : y = z) : (p @ q = p @ r) <~> (q = r) := equiv_inverse (equiv_whiskerL p q r).
imports: Basics.Overture Basics.Equivalences Basics.PathGroupoids Basics.Tactics