`{P : A -> Type} `{Q : B -> Type} (f0 : B -> A) (f1 : forall b:B, P (f0 b) -> Q b) (g g' : forall a:A, P a) (h : g == g') : ap (functor_forall f0 f1) (path_forall _ _ h) = path_forall _ _ (fun b:B => (ap (f1 b) (h (f0 b)))). Proof. revert h. equiv_intro (@apD10 A P g g') h. destruct h. simpl. transitivity (idpath (functor_forall f0 f1 g)). - exact (ap (ap (functor_forall f0 f1)) (path_forall_1 g)). - symmetry. apply path_forall_1. Defined.
Require Import Basics.Overture Basics.Equivalences Basics.PathGroupoids