`(f : B -> A) `(g : C -> D) (h h' : A -> C) (p : h == h') : ap (functor_arrow f g) (path_arrow _ _ p) = path_arrow _ _ (fun b => ap g (p (f b))) := @ap_functor_forall _ A (fun _ => C) B (fun _ => D) f (fun _ => g) h h' p.
Require Import Basics.Overture Basics.PathGroupoids Basics.Decidable Require Import Types.Forall.