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