Hi, all.

I am trying to understand the proof of proposition 7.6 in Shulman’s paper https://arxiv.org/pdf/1808.05204.pdf . I am interested in understanding it for applying it within SEAR to obtain interesting constructions (or ETCS, I say SEAR here because it comes with a collection axiom). One point that confuses me is that I am not yet familiar to the notion of stacks. As the claim is that the proof of 7.6 can be carried our within SEAR for each particular case, I think it would be ideal if I can see how the proof of 7.6 expands on particular examples to obtain a proof within SEAR. (Note: I do not think I am confused by how to apply the principle of replacement, I am confused by how its proof works for these particular examples. Say, from the context we can obtain from collection, how can we derive the existence of the context we want by manipulation within these examples without directly appeal to the replacement schema.)

For the simplest example I can think of, consider we want to build the well-ordered set N without explicitly defining the order “$lt$”. I think we may obtain an isomorphic copy of the well-ordered set N using replacement.

Let U be N, u be a natural number n in N, we can prove for each n there exists a set A and a relation R on A, such that R is a well order on A. That is, the context $\Theta$ is $[A,R:A\looparrowright A]$, and it can be proved that consider the formula $\phi$ such that $\phi(N,n,A,R:A\looparrowright A)$ is true iff $A$ has cardinality $n$ and $R$ is a well-order on $A$, then there would be a context over a cover $p:V \to N$ which descents to a context over $N$, and the resultant context should consist of a set $\tilde{A}$ and a relation on $\tilde{A}$, where $\tilde{A}$ has a map to $N$, call it $q$. I think then $q^{-1}(n)$ will be the well-ordered set contains $n$ elements, and the whole $\tilde{A}$ is the disjoint union of $A_0,\cdots,A_n,\cdots$. where $A_n$ is the well-ordered set containing $n$ elements. Then we can collect the maximal elements in each such set and obtain a copy of $N$ with the order $\lt$.

This example above is due to myself and I am not sure if I have got it correct, but the following example from Mike Shulman must be correct. It is a bit complicated and let me expand the story in details below.

For an ordinal $\alpha$, there is a notion of the $\alpha$-th Beth number, denoted as $\beth_\alpha$. This **number** itself is a **set**, so you may think of associate each ordinal with a set.

If $\alpha \lt \omega$, means that $\alpha$ is a finite ordinal, that is, a natural number, then the $\alpha$-th Beth number is the power set That is, , $P^\alpha(\mathbb N\beth_0 =\mathbb N\beth_1= PN$, $\beth_2 = PPN$ and $\beth_3 =PPPN$, etc.

Now consider the notion of the $\omega$-th Beth number, $\beth_\omega$ is defined to be the minimal set such that for every natural number $n$, the set $\beth_n$ injects to it. We are going construct $\beth_\omega$, and its construction relies on schema of replacement.

Regarding how to apply the replacement schema (credit to Mike Shulman):

The way to use replacement of contexts here is something like the following. For simplicity consider the natural numbers N. For x in N, consider the context consisting of a set X, a function p : X -> N, a relation R from X to X, and a function z : N -> X. Depending on x and on this context, consider the statement that the image of p is {y | y <= x}, that z is an isomorphism onto the fiber p^{-1}(0), and that R is the union of “membership” relations witnessing that p^{-1}(y+1) is the powerset of p^{-1}(y) for all y<x. One can prove by induction on x that two contexts satisfying this statement are uniquely isomorphic. Therefore, by replacement of contexts, there is a universal such context over N, which in particular has a function p : X -> N x N. Pulling this back along the diagonal map of N, we obtain an N-indexed family of sets that is the sequence of iterated powersets starting with N, and thus its total space is beth_omega.

Recall the statement of replacement of contexts (from Shulman’s paper):

for any formula $\phi(U, u :\in U, \Theta)$, for any $U$, if for every $u :\in U$ there is an extension $\Theta$ of $(U, u)$ such that $\phi(U, u, \Theta)$, and moreover this extension $\Theta$ is unique up to a unique isomorphism of contexts $\Phi_\Theta$, then there is an extension $\Theta_0$ of $(U ^* U,\Delta U )$ in $Set/U$ such that $\phi(U, u , u ^ * \Theta_0 )$ for all $u :\in U$.

Here the $\phi$ is the “statement” in ” consider the statement that the image of p”. This statement is on the following parameters: 1. The fixed natural number $x$, as in “For x in N, consider…”. 2. the function $p:X\to N$, 3. the relation $R:X\looparrowright X$, which is “the union of “membership” relations witnessing that p^{-1}(y+1) is the powerset of p^{-1}(y) for all y<x”. (Union of relations are given by consider a relation from $X$ to $Y$ as a subset of the power set ${\cal P} (X\times Y)$). 4. the funcion $z:N\to X$, which injects $N$ to $X$.

Intuitively, this relation says that $X$ is a set which is fibred over $N$ via the projection map $p:X\to N$, such that the fibre of $0$ is $N$, and for each number $m\lt n$ the fiber of its successor $m+1$ is the power set of the fiber of $m$. (*) Therefore, $\beth_n$ is the fiber of $n$.

Call the predicate by $Upow(n,p:X\to N,R:X\looparrowright,z:{N}\to X)$, we apply replacement of contexts on $Upow$. Here $U$ is $N$, $u\in U$, is $n\in N$, $\Theta$ is the list $[X,p:X\to { N},R:X\looparrowright X, z:{ N} \to X]$. As suggested by

One can prove by induction on x that two contexts satisfying this statement are uniquely isomorphic.

By induction on $n\in N$, we prove there exists a context $[X,p:X\to { N},R:X\looparrowright X, z:{ N} \to X]$ up to unique isomorphism such that $Upow(n,p:X\to N,R:X\looparrowright X,z:{ N}\to X)$. Therefore we can apply replacement. It gives a context $\Theta_0:=[X_0(\to N),p_0:X_0\to { N}\times { N}, R_0:X_0\looparrowright X_0,z_0:{\Bbb N}\times {N}\to X_0]$ where the maps $p_0,z_0$ and the relation $z_0$ are in the slice category. In particular, the fibre of the map $p_0:X_0\to { N}\times { N}$ on the point $(n,n)$ is the greatest fiber, i.e., the fiber of $n$ as in (*) above, of a context satisfying $Upow(n,p:X\to N,R:X\looparrowright,z:{ N}\to X)$. Therefore, pulling back along the diagonal map just means take out all these sets $\beth_1,...,\beth_n,\beth_{n+1},...$ (infinitely many). All these sets are contained as a subset of $X_0$, so we can take union of them.

Could someone please explain the proof of 7.6 in Shulman’s paper, in terms of some examples such as the two above, to illustrate how the proofs work? It does not have to be convoluted. I am most confused by the step which uses “Set is a stack of its regular topology”.

]]>Hi, all.

I would like to understand hoe does SEAR Axiom 5 works, that is Axiom of collection in SEAR.There is a section on “Application of Collection” and a sentence “(more detail to be added here…)”. My question is basically “what is intended to be there” in short.

According to my current understanding the example in this incomplete section, which aims to construct the ghost of $\{P^n(N)\mid n\in N\}$ should work as follows: we have a predicate taking a natural number $n$ and a set $Pn$, such predicate holds if $Pn \cong P^n(N)$ (here $\cong$ means bijection, cannot use equality here because the nlab page claims that there is no equality between sets.). And by axiom 5, we have a set $B$, a function $p:B\to N$. and a $B$-indexed family of sets $M:B\looparrowright Y$ such that for any $b\in B$, $M_b \cong P^{p(b)}( N)$ and for any $n\in N$, there exists a member of$b$ which is mapped to $n$. (because $P^n(N)$ exists for every $n$).

Does this sound correct?

If so, then it seems to me that the application of Axiom 5 only gives $Y$ contains $\coprod_{n\in N}P^n(N)$. As the nlab page claims that the collection axioms plays a similar role as replacement. How can I demonstrate that the thing I have obtained here is useful enough to be an analogue of the set $\{P^n( N)\mid n\in N\}$ as in ZF?

Other examples on SEAR Axiom 5 would also be nice! Thank you!

]]>Hi, all.

I am reading the SEAR nlab page here: https://ncatlab.org/nlab/show/SEAR

Regarding Theorem 2.8, it says:

Theorem 2.8. For any sets A and B, $A\times B$ is a product of A and B in the category Set, and a coproduct in the category Rel.

and the proofs says just in naive set theory.

But the coproduct of Rel in naive set theory is the disjoint union! I am confused how can $A\times B$ can serve as the coproduct of Rel, I know that the coproduct/product in Rel is the disjoint union, but how can the cartesian product coincide with the disjoint union? Given relation $f:A\to X,g:B\to X$, how can we define the relation $A \times B \to X$ so it is a coproduct?

I assume the inclusion relations $A\to A \times B$ and $B\to A\times B$ is $(a,(a1,b1))$ holds iff $a = a1$, and $(b,(a1,b1))$ holds iff $b = b1$. I may also make mistake here but I still wonder what else could it be.

Thank you for any explaination! (and sorry if it turns out to be a stupid question…)

]]>1) Is there a formalization of SEAR anywhere, like for example as a Coq/Agda/Lean library or the like? Just being able to see a fully formalized version & proving the basic theorems would help a lot. As I understand it, full SEAR requires some kind of dependent types in order to express indexed families of sets, and "property" as expressed in the nLab needs some kind of definition?

2) If you remove replacement to get the ETCS-like fragment, can the axioms be expressed purely in first order logic? Or does it still need some form of type theory? What gets lost, other than not being able to formulate products of an arbitrary number of non-isomorphic sets?

3) (possibly trivial but not immediately obvious since I have a hazy understanding of what is allowed by the axioms) In that first order fragment, is it provable that the lattice of relations from A to B is complete, since infinite conjunctions and disjunctions are generally not allowed? ]]>