Ancestors

Written by Oscar Cunningham on 2025-01-09 at 20:13

So in HoTT everything automatically respects the principle of equivalence, and it's impossible to write down something that doesn't. Whereas in ZFC we have the ability to do evil and we have to choose not to. Kinda feels like a snake got someone to eat an apple.

=> More informations about this toot | More toots from OscarCunningham@mathstodon.xyz

Toot

Written by Simon Tatham on 2025-01-10 at 09:57

@OscarCunningham I think one could probably make the isomorphic joke in programming languages, with 'safe by default' languages on the HoTT side (both Rust, and the larger and more established GC family) and 'close to the metal' languages on the ZFC side (most famously C and C++ these days, but also many other older languages).

In programming, there are two reasons for the unsafe languages to exist.

1. They're easier to invent and implement, so they came first; safe languages came along later.

2. They're a necessary substrate for implementing the safe languages. E.g. the (usual) Python interpreter is written in C, and the standard library used by safe Rust code has unsafe Rust inside it.

I guess HoTT is indeed newer than ZFC, paralleling reason 1. But reason 2 seems to have no analogue here.

=> More informations about this toot | More toots from simontatham@hachyderm.io

Descendants

Written by Oscar Cunningham on 2025-01-11 at 10:04

@simontatham There is a similar situation to 2. You can define 'homotopy type' in ZFC by modelling them as CW complexes or simplicial sets. You can then prove that the homotopy types you've defined obey the HoTT axioms. Thus any proof in HoTT also proves something about this interpretation in ZFC.

=> More informations about this toot | More toots from OscarCunningham@mathstodon.xyz

Written by Simon Tatham on 2025-01-11 at 11:16

@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 | More toots from simontatham@hachyderm.io

Written by soaproot on 2025-01-11 at 16:09

@simontatham @OscarCunningham Hmm, OK, thanks for saying that about limited HoTT knowledge. I did try to learn type theory in detail and the experience largely led me to learn set theory. There are many concepts which can be translated between the two. For example the difference between https://us.metamath.org/ileuni/ctiunct.html and https://us.metamath.org/ileuni/omiunct.html would be in type theory a sigma type (Σ) versus a truncated sigma type (∃), although the links I give are framed in the language of set theory.

=> More informations about this toot | More toots from soaproot@sfba.social