fact: Definition equiv_extension_along_pforall `{Funext} {A : pType} (P : pFam A) : ExtensionAlong@{Set _ _ _} (unit_name (point A)) P (unit_name (dpoint P)) <~> pForall A P.
imports: Basics Types PathAny WildCat Truncations.Core ReflectiveSubuniverse Extensions