fact: Definition ap_path_prod {A B C : Type} (f : A -> B -> C) {z z' : A * B} (p : fst z = fst z') (q : snd z = snd z') : ap (fun z => f (fst z) (snd z)) (path_prod _ _ p q) = ap011 f p q.
imports: Basics.Overture Basics.Equivalences Basics.PathGroupoids Basics.Tactics Basics.Trunc Basics.Decidable Types.Empty