fact: Definition sq_ap011 {A B C} (f : A -> B -> C) {a a' : A} (p : a = a') {b b' : B} (q : b = b') : PathSquare (ap (fun x => f x b) p) (ap (fun x => f x b') p) (ap (f a) q) (ap (f a') q).
imports: Basics Types.Paths Types.Prod DPath