Lemma functtransportb {X Y : UU} (f : X -> Y) (P : Y -> UU) {x x' : X} (e : x' = x) (p : P (f x)) : transportb (λ x, P (f x)) e p = transportb P (maponpaths f e) p. Proof. intros. induction e. apply idpath. Defined.