proposition: Lemma ap_path_sigma_1p {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: Proof. destruct p; reflexivity. Defined.
imports: HoTT.Basics Types.Arrow Types.Paths