@OscarCunningham I admit to knowing very little about HoTT in detail – I tried reading about it but ran out of motivation when the complicated 'equivalence types' business was presented without anything I recognised as a motivating example.
But that sounds to me more like an analogue of the Church-Turing thesis, in which any basically sensible model of computation can emulate any other in full, and hence they can all compute the same set of things. If you can make a matchstick model of HoTT inside ZFC and prove it obeys the HoTT axioms, surely you can make a similar model the other way round, maybe introducing a single HoTT type representing "a set in my ZFC model"?
I think it's not a convincing analogue of my point 2 unless you can't prove anything useful about HoTT without having ZFC first, so that even in a world where everyone wanted to exclusively use HoTT, you still wouldn't be able to throw away ZFC completely.
=> More informations about this toot | View the thread | More toots from simontatham@hachyderm.io
=> View OscarCunningham@mathstodon.xyz profile
text/geminiThis content has been proxied by September (3851b).