`{Funext} {A B C : Type} (p : A = B) (q : B = C) : equiv_path A C (p @ q) = equiv_path B C q oE equiv_path A B p. Proof. apply path_equiv, path_arrow. nrapply transport_pp. Defined.
Require Import HoTT.Basics. Require Import Types.Sigma Types.Forall Types.Arrow Types.Paths Types.Equiv Types.Bool Types.Prod.