|
|
|
|
|
|
by gallabytes
3990 days ago
|
|
|
We have something between the two in HoTT - universes of types is stratified by homotopy levels, corresponding to how many dimensions of structure a type has. A space with only points is thus a 0-type, a space with at most 1 point is a -1-type, and a space with only one is a -2-type. The catch is that univalence is inconsistent with LEM at h-levels greater than -1, but assuming it is perfectly consistent for -1 types, which can be thought of as the "at most true" propositions of classical logic. |
|
|