`{Funext} {A : pType} {B B' : pFam A} (f : forall a, B a <~> B' a) (p : f (point A) (dpoint B) = dpoint B') : pForall A B <~> pForall A B'. Proof. refine (issig_pforall _ _ oE _ oE (issig_pforall _ _)^-1). srapply equiv_functor_sigma'. 1: exact (equiv_functor_forall_id f). intro s; cbn. refine (equiv_concat_r p _ oE _). apply (equiv_ap' (f (point A))). Defined.
Require Import Basics Types. Require Import Pointed.Core.