Lemma. Transport ignores constant components [00EH]

For path in the identity type of cartesian decompositions and any , we have

This Lemma can probably be generalized.

Proof. Let

Define . In other words . Thus

Note that

Let and , then