Add category of ω-sets

[dschepler]

As discussed in the PR for the effective topos (#353), this PR is working on putting in the subcategory of ω-sets (otherwise known as a special case of the category of assemblies for the partial combinatory algebra also used in constructing the effective topos). The subcategory has simpler definitions that are easier to work with, to work up to the full definition of the effective topos. It can also be useful in an alternate construction of the effective topos, as the ex/reg completion of this category.

[dschepler]

Currently unresolved properties (many similar to the ones that were unresolved for the full effective topos):
is accessible
is Barr-coexact
is coaccessible
has effective cocongruences
has an extremal cogenerating collection
has an extremal cogenerator
has an extremal generating collection
has an extremal generator
is ℵ₁-accessible
has ℵ₁-cofiltered limits
has ℵ₁-filtered colimits

At this point, I think the best way to prove effective cocongruences would be to incorporate the proof from the abandoned quasitopos + SepPsh(X) PR, that regular + extensive + quotients of congruences -> effective cocongruences.

Otherwise, I might be able to adapt the proof from the effective topos PR to show that the $\omega$-sets with underlying sets contained in $\mathbb{N}$ are an extremal generating collection - though I haven't quite gotten the details on that down yet.

[dschepler]

On reviewing it myself, I see a need to improve the wording where I refer to a partial recursive function $\mathbb{N} \dashrightarrow \mathbb{N}$ "being a map as in the definition" for a function between the underlying sets. Maybe we can come up with a good name for that partial recursive map - something like "a realizer tracking map for $f$" perhaps?

[dschepler]

I'm not really happy with this proof as it stands -- there are a lot of moving parts to keep track of, and I get the feeling it will probably be confusing for many readers, especially the fourth paragraph on converting a map from the pullback to a generalized element of the relative exponential. I'm not sure at the moment what would be a good way to improve the presentation, though. So if you have any suggestions along those lines, they would certainly be welcome.

[dschepler]

Hmm... It might be possible to define a "regularly partial morphism classifier" $\tilde Y$ whose underlying set is $Y \sqcup { undef }$ and whose realization relation is that everything realizes $undef$, while $n$ realizes $y$ in $\tilde Y$ if and only if $n$ is a code for a partial recursive function such that $n \cdot 0 \downarrow$ and $n \cdot 0$ is a realizer for $y$ in $Y$. That means a morphism $X \to \tilde Y$ should be equivalent to a regular subobject $X'$ of $X$ and a morphism $X' \to Y$. (The indirection in realizers is necessary in order to have something to do with realizers of elements in $X$ which aren't necessarily realizers of any elements of $X'$.) I should also be able to show directly that the category is cartesian closed, using the simplified definition, and then adapt one of the standard proofs that a topos is locally cartesian closed to this situation (constructing $[X, Y]_Z$ as an equalizer of two certain maps from $[X, \tilde Y] \times Z$).

[ScriptRaccoon]

I'm not really happy with this proof as it stands -- there are a lot of moving parts to keep track of, and I get the feeling it will probably be confusing for many readers, especially the fourth paragraph on converting a map from the pullback to a generalized element of the relative exponential. I'm not sure at the moment what would be a good way to improve the presentation, though. So if you have any suggestions along those lines, they would certainly be welcome.

I am not there yet to go through the mathematics of the proofs, but I have some suggestions regarding the layout, which often helps with understanding a proof (when done right).

Currently, the proof has a few paragraphs, but still, it is a long wall of text.

My suggestions are:

• use the vertical space generously (in particular after Add button to expand popups to full height #316 !)
• use as much paragraphs as you like
• use displayed formulas more often
• for long or complex proofs, use html to add sections to the proof

Doing these adjustments, it looks much better and is easier to read, and probably also to understand.

You can find the adjusted proof here: proof.txt

This is just my first shot. It could even be improved much further (but for this, I would need to digest the proof).

Also, formulas are ok! Language can sometimes be more confusing, and in any case, it is more lengthy. I write this because you tend to explain things with words instead of just writing them down with formulas. (Of course, formulas without explanation are also bad, but you typically spend most words with describing formulas.) Also, you often work with functions without ever giving them a name, and then you need to spend words later to remind the reader which function you mean. Using a symbol will be easier.

For example, I would replace

We then claim that $E$ with the restriction $R_E$ of the above realization relation forms a relative exponential of $f$ and $g$ in $\omega{-}Set$. First, it is easy to see that the restriction of $h$ to $E$ is a morphism of $\omega$-sets $(E, R_E) \to (Z, R_Z)$, with $p_1 : N \to N$ working as the partial recursive function in the definition. This is the morphism we will use to consider $(E, R_E)$ as an object of $\omega{-}Set / (Z, R_Z)$.

with (after having named the realization relation $R$)

Then $(E,R|_E)$ is an $\omega$-set, and $h|_E : (E, R|_E) \to (Z, R_Z)$ is a morphism of $\omega$-sets with realization function $p_1 : N \to N$. We claim that $h|_E$ is the exponential of $f$ and $g$ in $\omega{-}Set / (Z, R_Z)$.

It is much shorter, but tells exactly the same.

(this also fixes an incorrect abuse of notation that does not distinguish a morphism from its domain, which is quite common for slice categories, but not necessary either.)

I know that this is a superficial analysis at this point, but I think it already helps to make the proof easier to understand. I will write more once I actually look at the mathematics.

General tip for longer proofs: Preview and author the math on a temporary content page, which is easier to author and to refresh.

[ScriptRaccoon]

Hmm... It might be possible to define a "regularly partial morphism classifier" [...]

A more "pedestrian" and "educational" approach:

1. First give a full proof that the category is cartesian closed.
2. Then give a full proof that the category is even locally cartesian closed, and explain which changes are necessary.

Compare this with Set. I don't think any beginner in category theory will even be able to understand the proof that Set is locally cartesian closed without first having understood why it is cartesian closed (independently from the fact that there are proofs reducing the properties to one another).

[dschepler]

I think it could clean things up to define $X_z$ as $f^({z})$ with the restricted realization relation, and similarly for $Y_z := g^({z})$. Then the underlying set of the relative exponential is $\bigsqcup_{z\in Z} Hom(X_z, Y_z)$, and it's natural to define a realizer of an element as a pairing of a realizer of $z$ and a code for the realizer transformer of the morphism. Then the proofs should hopefully look a lot like $z$-parameterized versions of the proofs for cartesian closure that I just added.

[ScriptRaccoon]

On reviewing it myself, I see a need to improve the wording where I refer to a partial recursive function N ⇢ N "being a map as in the definition" for a function between the underlying sets. Maybe we can come up with a good name for that partial recursive map - something like "a realizer tracking map for f " perhaps?

I have no expertise on this category at all, but I would probably call it "a realization function of the morphism", or simply "a realizer of the morphism". Then you can describe morphisms as realizable functions.

EDIT. after reading some of the proofs (still on a superficial level), I think that any term will greatly simplify the exposition; it will be used all the time

[ScriptRaccoon]

Is this new implication an answer to https://mathoverflow.net/questions/513430 because it makes all these assignments redundant?

I noticed that Example 3.14 is now only used for Top_* and PMet (and Met).

[dschepler]

I guess it's a partial answer, given that it only works for the extensive categories (with coequalizers) where you can find a non-effective cocongruence. If I remember correctly, I traced through the proof in the case of Top and it gave this pullback of a regular epimorphism which isn't a regular epimorphism:
$$\begin{CD}
{ a, d }_d @>>> { a, d }_i \
@vvv @vvv \
{ a, b }_i \sqcup { c, d }_i @>>> { a, b = c, d }_i
\end{CD}$$

[ScriptRaccoon]

I find $E \xleftarrow{p\circ i_2} X \xrightarrow{p\circ i_1} E$ confusing since $i_1,i_2$ mean something different in the diagram below.

Can we maybe state the proof using a pair $p_1, p_2 : X \rightrightarrows E$? (This is my general recommendation for (co)congruences in CatDat. Working with pairs has made several things more clear to me.)

Also expressions like $p(r(e))$ are confusing (used below) since the codomain of $r$ is not the domain of $p$. You actually mean $p(i_1(r(e))$. It is easer to write directly $p_1(r(e))$.

I would then also remove the usage of $X'$ and $E'$. I have suggested this notation before, but I don't think anymore that it is good (at least, in this proof).

If you agree, I would also suggest to rework regular_epi-regular_extensive_consequences in the same way.

[ScriptRaccoon]

It is a bit confusing that you first choose $e_1,e_2$ and then claim that "Then we have two retractions ..." even though their construction is independent of $e_1,e_2$. Isn't this a general lemma about cocongruences that we might extract?

The lemma is especially clear in the dualized version with generalized elements, i.e. w.l.o.g. in Set. If $R$ is an equivalence relation on $X$, we have $t : R \times_X R \to R$ mapping $((a,b),(b,c)) \mapsto (a,c)$, and it has two sections $(a,c) \mapsto ((a,a),(a,c))$ and $(a,c) \mapsto ((a,c),(c,c))$.

[ScriptRaccoon]

It is confusing to write $e \mapsto \cdots$ in the definition of $s_1$. You actually mean (and use!) $i_1(e) \mapsto \cdots$.

[ScriptRaccoon]

I suggest to use more displaystyle formulas in this paragraph.

[ScriptRaccoon]

This is intuitively clear to me, but how can we use the definition of extensivitiy precisely here?

[dschepler]

If you have morphisms $U \to E$ and $U \to E + E'$ with equal compositions to $E +_X E'$, then use extensionality to split the second into $U_1 \to E$ and $U_2 \to E'$ with $U \cong U_1 + U_2$; then the individual pullbacks induce morphisms $U_1 \to X$ and $U_2 \to X'$, and their sum gives the required morphism $U \to X + X'$.

[ScriptRaccoon]

Do we want to remove it then from the content page?

[dschepler]

I guess we could also keep it in with check_redundancy: false

[ScriptRaccoon]

Quite amazing that these non-trivial proofs for Bin and Meas can be removed.

[ScriptRaccoon]

Currently unresolved properties [...]

With all of the categories that I have added in the last weeks, I have decided every single property. This was a lot of work, but Gemini Pro has helped me a lot to find the proofs (I can recommend using it), and I think the database has the best value when there are no questions left. But, of course, if something just does not work, leave it open and/or write an issue.

[ScriptRaccoon]

Can we give a description of this category that is accessible for readers without looking at the effective topos? Because this was the initial goal: make the construction of the effective topos easier to follow. So the references should (mostly) go only in one direction.

For example: what is an intuitive picture for the pair $(X,R_X)$? Why do we say that $n$ realizes $x$ when $(n,x) \in R_X$? This seems to be hinting at some interpretation, but this interpretation is never mentioned. Maybe the word "assembly" is also relevant.

I don't have answers to these questions. I still try to understand the basics here.

Maybe this information can also be added to the linked nLab article.

[dschepler]

I also haven't found motivation for the definitions in any of the sources I've found, except that in the end it gives a topos with desirable properties of the internal logic.

Though I suppose a possible inkling of an answer in the form an example could be: You could fix an enumeration of the intervals in $\mathbb{R}$ with rational endpoints, and then define an $\omega$-set whose underlying set is $\mathbb{R}$ and whose realization relation is that $n$ realizes $x$ exactly when $x$ is in the $n$th interval. Then for $f : \mathbb{R} \to \mathbb{R}$, a compatible realizer transformer would correspond to a sound approximation of $f$ in terms of "interval arithmetic".

Though that example also has its shortcomings. Namely, in interval arithmetic, you usually also care whether the approximation more or less has some reasonable "tightness" properties, whereas the category of $\omega$-sets doesn't care in the least about tightness for that example, only about soundness. Also, the morphisms do not contain any particular realizer transformer in their data, only the existence of at least one is required. (So, I think most "naturally occurring" locally bounded functions $\mathbb{R} \to \mathbb{R}$ will be morphisms in that category, except for pathological examples such as applying the Busy Beaver function to the floor of $x$.)

So very roughly, I've sort of been thinking of an $\omega$-set as an abstract set but where there are some "pieces of information" about elements of the set which have some "computational relevance".

[ScriptRaccoon]

This can also be explained by using the fact (mentioned in the proof for epis, but maybe one can make this more prominent) that $X \mapsto (X, N \times X)$ is right adjoint to the forgetful functor, and right adjoints preserve terminal objects.

[dschepler]

I was also thinking that I could eventually add both functors to the database, along with some corresponding functors for the effective topos (the right adjoint is conventionally called $\nabla$, though that's also the name of a similar right adjoint for the effective category, so I would probably call them $\nabla_{\omega{-}Set}$ and $\nabla_{Eff}$ respectively), and also a couple functors between $\omega{-}Set$ and $Eff$.