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