[boyobo]

Now I'm not sure what your point is. Are you suggesting that HoTT is to python as ZFC is to turing machine tape?

[zrkrlc]

Nitpick, but I think what you meant to say what "HoTT is to ZFC as Python is to Turing machine tape". Hope it helps.