Definition transport_b_b {X : UU} (P : X ->UU) {x y z : X} (e : x = y) (e' : y = z) (p : P z) : transportb P e (transportb P e' p) = transportb P (e @ e') p. Proof. intros. induction e'. induction e. apply idpath. Defined.