Toot

Written by Martin Escardo on 2025-01-14 at 20:30

@ncf

It makes a difference whether you ask this question externally or externally.

I haven't thought about the external question.

But if "every type has split support" is interpreted internally, then every object has decidable equality, including the object of truth values, and hence excluded middle holds (the topos is boolean). Conversely, if the topos is boolean, then every type has split support.

https://lmcs.episciences.org/3217

=> More informations about this toot | View the thread | More toots from MartinEscardo@mathstodon.xyz

Mentions

=> View ncf@types.pl profile

Tags