{A : Type} (P : A -> Type) (x : A) (y1 y2 : P x) (q : y1 = y2) : ap (exist P x) q = path_sigma' P 1 q. Proof. destruct q; reflexivity. Defined.
Require Import HoTT.Basics. Require Import Types.Arrow Types.Paths.