`{P : A -> Type} `{Q : B -> Type} (f : A -> B) (g : forall a, P a -> Q (f a)) (u v : sig P) (p : u.1 = v.1) (q : p # u.2 = v.2) : ap (functor_sigma f g) (path_sigma P u v p q) = path_sigma Q (functor_sigma f g u) (functor_sigma f g v) (ap f p) ((transport_compose Q f p (g u.1 u.2))^ @ (@ap_transport _ P (fun x => Q (f x)) _ _ p g u.2)^ @ ap (g v.1) q). Proof. destruct u as [u1 u2]; destruct v as [v1 v2]; simpl in p, q. destruct p; simpl in q. destruct q. reflexivity. Defined.
Require Import HoTT.Basics. Require Import Types.Arrow Types.Paths.