Definition famhomothomothomot {X : UU} {P Q : X -> UU} (h1 h2 : P ~ Q) (H : h1 ~ h2) : famhomotfun h1 ~ famhomotfun h2. Proof. intros. intro xp. apply (maponpaths (λ q, tpair Q (pr1 xp) q)). induction (H (pr1 xp)). apply idpath. Defined.