search

martinescardo / TypeTopology

Logical manifestations of topological concepts, and other things, via the univalent point of view.
GNU General Public License v3.0
220 stars 40 forks source link

If the flat natural numbers are ω-complete, then LPO holds #289

Closed tomdjong closed 3 weeks ago

martinescardo commented 3 weeks ago

Nice! I have one minor "complaint". In CoNatutorals/Sharp we define

ℕ⊥ = 𝓛 ℕ

and call this the flat natural numbers.

Now you have something else called the same, with the same notation.

At least a warning would be needed, saying that one of them is the one that works constructively, and the other one is the classical definition (and that they are equivalent classically).

(I forget what we call things in our papers and in your thesis.)

Everything else in the PR is fine.

tomdjong commented 3 weeks ago

Thanks @martinescardo! I added a warning.