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? ]]>