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.