fact: Definition equiv_path_pp `{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.
imports: HoTT.Basics Types.Sigma Types.Forall Types.Arrow Types.Paths Types.Equiv Types.Bool Types.Prod