fact: Definition transport_Circle_code_loopV (z : Int) : transport Circle_code loop^ z = int_pred z.
imports: Basics Types Pointed.Core Pointed.Loops Pointed.pEquiv HSet Spaces.Pos Spaces.Int Colimits.Coeq Truncations.Core Truncations.Connectedness Cubical.DPath