Jon Sterling on Nostr: nprofile1q…g47dl W-types are foundationally extremely weak — they are no stronger ...

nprofile1qy2hwumn8ghj7un9d3shjtnyd968gmewwp6kyqpqlpv03u4n97y28cz0x69yp746p4ed9er23992cmg85pdx0dgxdcus7g47dl (nprofile…47dl) 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.