`{Funext} {A : pType} (P : pFam A) : ExtensionAlong@{Set _ _ _} (unit_name (point A)) P (unit_name (dpoint P)) <~> pForall A P. Proof. unfold ExtensionAlong. refine (issig_pforall A P oE _). apply equiv_functor_sigma_id; intro s. symmetry; apply equiv_unit_rec. Defined.
Require Import Basics Types. Require Import Homotopy.IdentitySystems. Require Import WildCat. Require Import Truncations.Core. Require Import ReflectiveSubuniverse. Require Import Extensions.