Add transportComposite

[lpw25]

This PR just adds the following definition to Transport.agda:

-- transporting along a composite path is equivalent to transporting twice
transportComposite : ∀ {ℓ} {A B C : Type ℓ} (p : A ≡ B) (q : B ≡ C) (x : A)
                 → transport (p ∙ q) x ≡ transport q (transport p x)
transportComposite = substComposite (λ D → D)

It's a fairly fundamental property, and whilst substComposite already exists that can be hard to find for newcomers looking for a result about transport.

[mortberg]

Looks good to me. Thanks for the contribution! I'll merge once the CI is finished