Freely transported terms in dependent type theory

2026-06-03 · type-theory cubical

Given $𝐴$ and $𝐵 : 𝐴 \to 𝐓𝐲𝐩𝐞$ we can make sense of transported terms along equalities between indices in $𝐴$ . Say, with

𝗌𝗎𝖻𝗌𝗍 : (𝑝 : 𝑎 = 𝑎') \to 𝐵 𝑎 \to 𝐵 𝑎'

for $𝑎, 𝑎' : 𝐴$ .

For instance, if $𝑝 : 𝑎 = 𝑎'$ and $𝑏 : 𝐵 𝑎$ then $𝗌𝗎𝖻𝗌𝗍 𝑝 𝑏 : 𝐵 𝑎'$

To avoid landing in transport hell, I suspect that it may be preferable to work inside of a description of freely transported terms instead of taking semantic transports. The hypothesis is that by using descriptions of formal transport rather than actually computing a transport, we may defer the computation of an actual transport until the end of a construction. So instead of working with $𝐵 𝑎$ directly, perhaps we may work with

𝖥𝗋𝖾𝖾𝖲𝗎𝖻𝗌𝗍 𝐵 𝑎 ≔ \sum_{(𝑎' : 𝐴)} \sum_{(𝑝 : 𝑎 = 𝑎')} 𝐵 𝑎'

I think that this is very closely related to the Fording trick, as a map out of $𝖥𝗋𝖾𝖾𝖲𝗎𝖻𝗌𝗍 𝐵 𝑎$ ,

𝑓 : \sum_{(𝑎' : 𝐴)} \sum_{(𝑝 : 𝑎 = 𝑎')} 𝐵 𝑎' \to 𝐶

can instead be described as a map,

𝑔 : (𝑎' : 𝐴) \to (𝑝 : 𝑎 = 𝑎') \to 𝐵 𝑎' \to 𝐶

Both this and the fording trick use the Coyoneda lemma to represent an dependent type family.