Identity type of cart-dec [00DY]

Fix a finite set . There is an equivalence

Where is the induced map from the paths and .

Proof. Denote by the type family .

In the second step, we make use of the rule:

For a path denote by the induced path . then for and we get a term of type

by doing path induction on : When , we get

So it suffices to provide a term of type , which is (up to unit-path) given by reversal of paths.