Transport in Species of Types [008P]

Let be a species of types and let , be types in the universe . Then for any equivalence of types , we get obtain a term of type as follows.

By univalence we upgrade to a path . Then transport gives us the desired map.