{A : pType} {B C : pFam A} (g : forall a, B a -> C a) (g₀ : g (point A) (dpoint B) = dpoint C) (f : pForall A B) : functor2_pforall_right (fun a => reflexivity (g a)) (phomotopy_reflexive f) (concat_1p _) ==* phomotopy_reflexive (functor_pforall_right g g₀ f). Proof. pointed_reduce. reflexivity. Defined.
Require Import Basics Types. Require Import Pointed.Core.