{A : pType} {B B' : A -> pType} (g : forall a, B a ->* B' a) (f : ppforall a, B a) : ppforall a, B' a. Proof. simple refine (functor_pforall_right _ _ f). + exact g. + exact (point_eq (g (point A))). Defined.
Require Import Basics Types. Require Import Pointed.Core.