{A B : Type} {P : A -> Type} (F : forall a, P a -> B) (a : A) {x y : P a} (p : x = y) : ap (fun w => F w.1 w.2) (path_sigma' P 1 p) = ap (fun z => F a z) p. Proof. destruct p; reflexivity. Defined.
Require Import HoTT.Basics. Require Import Types.Arrow Types.Paths.