Jon Sterling on nostr

nostr:nprofile1qy2hwumn8ghj7un9d3shjtnyd968gmewwp6kyqpqjd874v63430gng67kpw5m597f34dr9vr0yhkp8dkmnma8208raysj9xuzd I'm mostly doing algebraic geometry, so well-founded trees and so on don't really appe...

Jon Sterling @Jon Sterling 1770654775

@nprofile1q... W-types are foundationally extremely weak — they are no stronger than having a natural numbers object, and therefore exist in every non-finitist model of constructive mathematics that anyone would ever consider. That is why constructive type theorists do not have any concerns about W-types.

Jon Sterling · 25w

nostr:nprofile1qy2hwumn8ghj7un9d3shjtnyd968gmewwp6kyqpqlpv03u4n97y28cz0x69yp746p4ed9er23992cmg85pdx0dgxdcus7g47dl Of course, you probably do encounter well-founded things with some frequency in geometry, e.g. Noetherian assumptions, etc.

Jakob · 25w

nostr:nprofile1qy2hwumn8ghj7un9d3shjtnyd968gmewwp6kyqpqjd874v63430gng67kpw5m597f34dr9vr0yhkp8dkmnma8208raysj9xuzd Do you have a reference for this? https://ncatlab.org/nlab/show/transfinite+construction+of+free+algebras this does not look constructive to me, right?

Martin Escardo · 25w

nostr:nprofile1qy2hwumn8ghj7un9d3shjtnyd968gmewwp6kyqpqjd874v63430gng67kpw5m597f34dr9vr0yhkp8dkmnma8208raysj9xuzd writes "W-types are foundationally extremely weak — they are no stronger than having a natural numbers object". This is known to be the case only in the presence of propositional resi...