{A} {P : A -> Type} {f g h : forall x, P x} : pointwise_paths A P f g -> pointwise_paths A P g h -> pointwise_paths A P f h := fun p q x => p x @ q x. Global Instance reflexive_pointwise_paths A P : Reflexive (pointwise_paths A P). Proof. intros ? ?; reflexivity. Defined.