fact: Definition equiv_sq_dp {A B : Type} {f g : A -> B} {a1 a2 : A} {p : a1 = a2} {q1 : f a1 = g a1} {q2 : f a2 = g a2} : DPath (fun x => f x = g x) p q1 q2 <~> PathSquare q1 q2 (ap f p) (ap g p).
imports: Basics Types.Paths Types.Prod DPath