{A : pType} {B B' : pFam A} (f : forall a, B a -> B' a) (p : f (point A) (dpoint B) = dpoint B') (g : pForall A B) : pForall A B' := Build_pForall A B' (fun a => f a (g a)) (ap (f (point A)) (dpoint_eq g) @ p).
Require Import Basics Types. Require Import Pointed.Core.