Equality of conatural numbers

[fredrik-bakke]

We characterize equality of conatural numbers.

[fredrik-bakke]

I've started formalizing the alternative definition of the conaturals as the type of decreasing binary sequences alongside this, and I am wondering what name to use for it, what label to give the type, and in which namespace it should be placed. In Martín's formalizations, he calls it the "generic convergent sequence" and gives it the label ℕ∞ but that is already taken by our coinductive definition. I'm tempted to place the formalization of this alternative definition in set-theory, but am not sure if that is a good idea given that the conaturals are placed in elementary-number-theory. I suppose I prefer "decreasing binary sequences" over "generic convergent sequence", as the former leaves room for the equivalent "increasing binary sequences". Opinions or any input is appreciated!

[EgbertRijke]

We could consider reserving the infinity notation for things that are defined by adding a point at infinity, such as the one-point compactification. In that case the name for the conatural numbers would have to change to something like conat or conatural-number, which would make sense because as it is defined it is the dual to the natural numbers. I like decreasing-boolean-sequence-ℕ for the type of decreasing boolean sequence. We already have some sequence-ℕ definitions for sequences indexed by the natural numbers (as opposed to sequences indexed by the integers), so boolean-sequence-ℕ would be a sequence of booleans, and decreasing-boolean-sequence-ℕ would be a decreasing such sequence.

[EgbertRijke]

One more thought: If we would define one-point compactifications by specification, then we could prove that the conatural numbers is a one-point compactification of the natural numbers, justifying that the name can stay as it is.

[fredrik-bakke]

What do you mean by specification?

[EgbertRijke]

A specification of X is saying what it means to be an X, instead of defining an instance of an X.

The specification of one point compactification is its universal property, whereas "the" one point compactification would be an operation returning one point compactifications

[fredrik-bakke]

Right right. Thanks for clarifying!

[EgbertRijke]

All that was to say that I'm happy to keep the name ℕ∞ for the conatural numbers. So no need to change anything.

[fredrik-bakke]

This has got me thinking about what the universal property should be... Perhaps something like the following:

• An extension f : X ↪ X∞ equipped with a point ∞ ∈ X∞ is a one-point compactification of X if the double complement of the image of f is full, and ∞ ∈ X∞ satisfies some pointed compactness condition.

[fredrik-bakke]

In TypeTopology, Martín defines a limit point to be an element whose isolatedness implies WLPO. I would have hoped for something that is "model agnostic" to the natural numbers, so I think the following should work:

• An extension f : X ↪ X∞ equipped with a point ∞ ∈ X∞ is a one-point compactification of X if X∞ is compact, and the isolatedness of ∞ ∈ X∞ implies that X is compact.

[fredrik-bakke]

Aaand you need something to ensure uniqueness of ∞ of course. Perhaps "if x is not equal to ∞ then it is in the image of f."

[EgbertRijke]

The n-lab page has a more traditional approach to the universal property of one-point compactification:

https://ncatlab.org/nlab/show/one-point+compactification

[fredrik-bakke]

Aha, so do you have certain definitions in mind for the notions of "locally compact", "Hausdorff" and "closed subspace"?
I suppose closed subspace should be double negation stable, and Hausdorff should mean that the diagonal X -> X x X is double negation stable? I'm less sure about local compactness.

[fredrik-bakke]

I suppose this kind of stuff really ought to be in a type-topology namespace...

[fredrik-bakke]

Ah, so a Hausdorff type is really just a type whose equality is double negation stable, huh?

[EgbertRijke]

I suppose this kind of stuff really ought to be in a type-topology namespace...

Or in a condensed-mathematics namespace.

I don't have any concrete proposals for definitions of Hausdorff types or locally compact types right now, but it would be interesting to explore.

[fredrik-bakke]

If I dare ask, how is this condensed mathematics?

[fredrik-bakke]

To my very limited understanding reading up this afternoon, in the "traditional" interpretation of types as topological spaces, "closed" means double negation stable. Although, of course, as you and I both know, double negation is but one mode of logic.

[EgbertRijke]

If I dare ask, how is this condensed mathematics?

If I recall correctly, this sort of thing comes up in Reid Barton's interpretation of condensed mathematics.

[EgbertRijke]

To my very limited understanding reading up this afternoon, in the "traditional" interpretation of types as topological spaces, "closed" means double negation stable. Although, of course, as you and I both know, double negation is but one mode of logic.

Original, I meant "traditional" as in the way you'd learn about it in a standard textbook on topology. When people say traditional mathematics, it usually refers to mathematics in the standard curriculum and not really this kind of fancy stuff:)

[fredrik-bakke]

@EgbertRijke I'm going to need to start formalizing some omniscience/compactness/searchability properties of the conaturals and co. Since there is more than one way to interpret compactness in HoTT, I'm unsure what I should call the concepts. For instance, we already have sequentially compact types in the library, which is something very different. One way to go about it is to qualify it as "logically compact", I suppose.

The concepts I'm looking to formalize are the following, indexed by their TypeTopology names:

• is-Σ-compact/searchable/is-compact/is-Compact: A type $X$ is Σ-compact if for every decidable subtype $Y$ of $X$, either we constructively have an element of $Y$ or $Y$ is empty.
• is-∃-compact/LPO: A type $X$ is ∃-compact if for every decidable subtype $Y$ of $X$, either $Y$ is inhabited or $Y$ is empty.
• is-Π-compact/WLPO: A type $X$ is ∀-compact, if for every decidable subtype $Y$ of $X$, either $Y$ is full or $Y$ is not full.

Martín himself seems to have dropped the terminology "omniscient" and "searchable" in favor of compactness:

Because of the relation to LPO, we formerly referred to Σ- or
∃-compact sets as "omniscient" sets:

Martin H. Escardo, Infinite sets that satisfy the principle of
omniscience in any variety of constructive mathematics. The Journal
of Symbolic Logic, Vol 78, September 2013, pp. 764-784.
https://www.jstor.org/stable/43303679

And because of the connection with computation, we called them
exhaustively searchable, or exhaustible or searchable:

Martin Escardo. Exhaustible sets in higher-type computation. Logical
Methods in Computer Science, August 27, 2008, Volume 4, Issue 3.
https://lmcs.episciences.org/693

The name "compact" is appropriate, because e.g. in the model of
Kleene-Kreisel spaces for simple types, it does correspond to
topological compactness, as proved in the above LMCS paper.

The name "compact" is also adopted in Longley and Normann's book
"Higher-Order Computability" (Springer 2015).

We emphasize that here we don't assume continuity axioms, but all
functions are secretly continuous, and compact sets are secretly
topologically compact, when one reasons constructively.

[fredrik-bakke]

I'm going to use "searchable" for the constructive thing, "existentially compact" for ∃-compact and "universally compact" for ∀-compact for now. We can decide on what's best during a later review process.

[fredrik-bakke]

I'm opening this PR up to review. I've moved all of the work-in-progress, less relevant formalizations, to a different branch.