Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

• Forgot your password?
• Apply for membership

1. • CommentRowNumber1.
   • CommentAuthorYimingXu
   • CommentTimeApr 12th 2023
   • PermaLink
   Author: YimingXu
   Format: MarkdownItexHi, all. I am a bit confused by the proofs in "comparing material and structural set theories" https://arxiv.org/pdf/1808.05204.pdf My question is about proposition 7.5 (collection of contexts) and proposition 7.6 7.5 proves collection of contexts from collection of functions and collection of equalities. The proof says: >Simply apply collection of sets and functions repeatedly, using the fact that regular epimorphisms compose. To make sure I understand it correctly let me expand an example: say the context is $\{X,Y,f:A\to B\}$ over $U$, given that for each $u:1\to U$, there exists a context $X,Y, f:X\to Y$ such that $\phi(u,X,Y,f:X\to Y)$, to unwind this layer by layer, we can write $\exists X (\exists Y \;\exists f:X\to Y. \phi(u,X,Y,f))$. We set $\psi(u,X):= \exists Y \;\exists f:X\to Y. \phi(u,X,Y,f)$, then by collection of sets, for each $u:1\to U$, there exists a set $X$ such that $\psi(u,X)$. Then we get a regular epi $p:V\to U$ and a $p_A:A\to V$ such that for each $v:1\to V$, $\psi(pv, v^*A)$. And for the next layer, we use the fact that for each $v:1\to V$, we have $\exists Y.(\exists f.\phi(pv,v^*A,Y,f:v^*A \to Y))$ and set $\varphi(v,Y) := \exists f.\phi(pv,v^*A,Y,f:v^*A \to Y)$, then by collection of sets we have a regular epi $q:W\to V$ and a $f_B:B\to W$, such that for all $w:1\to W$, we have $\exists f. \phi(pqw,w^*q^*A,f:w^*q^*A \to B)$. Also, the composition $p\circ q$ is a regular epi $W\to U$. Next step is similar and use function collection instead. I think as replacement of sets and functions are also proved in paper, then the proof of replacement of context can be obtained the same way and be as short as "simply apply replacement of sets and functions repeatly". But the paper is not written like this. Did I miss some critical thing? I think the stack condition is only used for forming new sets, and prestack condition is sufficient to form the functions, given the sets are already constructed. We can only invoke the gluing facts in proving replacement of sets and functions as lemma, but not need to invoke them in the proof of replacement of context.

   Hi, all.

   I am a bit confused by the proofs in “comparing material and structural set theories” https://arxiv.org/pdf/1808.05204.pdf

   My question is about proposition 7.5 (collection of contexts) and proposition 7.6

   7.5 proves collection of contexts from collection of functions and collection of equalities. The proof says:

   Simply apply collection of sets and functions repeatedly, using the fact that regular epimorphisms compose.

   To make sure I understand it correctly let me expand an example: say the context is $\{X,Y,f:A\to B\}$ over $U$, given that for each $u:1\to U$, there exists a context $X,Y, f:X\to Y$ such that $\phi(u,X,Y,f:X\to Y)$, to unwind this layer by layer, we can write $\exists X (\exists Y \;\exists f:X\to Y. \phi(u,X,Y,f))$. We set $\psi(u,X):= \exists Y \;\exists f:X\to Y. \phi(u,X,Y,f)$, then by collection of sets, for each $u:1\to U$, there exists a set $X$ such that $\psi(u,X)$. Then we get a regular epi $p:V\to U$ and a $p_A:A\to V$ such that for each $v:1\to V$, $\psi(pv, v^*A)$. And for the next layer, we use the fact that for each $v:1\to V$, we have $\exists Y.(\exists f.\phi(pv,v^*A,Y,f:v^*A \to Y))$ and set $\varphi(v,Y) := \exists f.\phi(pv,v^*A,Y,f:v^*A \to Y)$, then by collection of sets we have a regular epi $q:W\to V$ and a $f_B:B\to W$, such that for all $w:1\to W$, we have $\exists f. \phi(pqw,w^*q^*A,f:w^*q^*A \to B)$. Also, the composition $p\circ q$ is a regular epi $W\to U$. Next step is similar and use function collection instead.

   I think as replacement of sets and functions are also proved in paper, then the proof of replacement of context can be obtained the same way and be as short as “simply apply replacement of sets and functions repeatly”. But the paper is not written like this. Did I miss some critical thing? I think the stack condition is only used for forming new sets, and prestack condition is sufficient to form the functions, given the sets are already constructed. We can only invoke the gluing facts in proving replacement of sets and functions as lemma, but not need to invoke them in the proof of replacement of context.

2. • CommentRowNumber2.
   • CommentAuthorMike Shulman
   • CommentTimeApr 17th 2023
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexThe hypothesis of replacement of contexts asserts that the extension is unique up to a unique isomorphism *of contexts*. This doesn't entail that each piece of the context, type or function, is separately unique up to a unique isomorphism. Uniqueness of the isomorphisms are only assumed as a unit.

   The hypothesis of replacement of contexts asserts that the extension is unique up to a unique isomorphism of contexts. This doesn’t entail that each piece of the context, type or function, is separately unique up to a unique isomorphism. Uniqueness of the isomorphisms are only assumed as a unit.

3. • CommentRowNumber3.
   • CommentAuthorYimingXu
   • CommentTimeApr 27th 2023
   • (edited Apr 27th 2023)
   • PermaLink
   Author: YimingXu
   Format: MarkdownItexThank you for your response! I see this part. But then, there is also a line saying: >The assumption implies that when pulled back along any $z : 1 \to V\times_{U} V$, these two contexts become uniquely isomorphic. Thus, by replacement of functions and equalities applied some finite number of times, we actually have a unique isomorphism $r^*\Theta \cong s^*\Theta$ in $Set/V \times_U V$ Over each element $z:1\to V\times_{U}V$, the isomorphism is still an isomorphism of contexts, for each object or arrow we still do not have they are unique. So how can we apply "replacement of functions and equalities" finitely many times to get the unique isomorphism?

   Thank you for your response! I see this part. But then, there is also a line saying:

   The assumption implies that when pulled back along any $z : 1 \to V\times_{U} V$, these two contexts become uniquely isomorphic. Thus, by replacement of functions and equalities applied some finite number of times, we actually have a unique isomorphism $r^*\Theta \cong s^*\Theta$ in $Set/V \times_U V$

   Over each element $z:1\to V\times_{U}V$, the isomorphism is still an isomorphism of contexts, for each object or arrow we still do not have they are unique. So how can we apply “replacement of functions and equalities” finitely many times to get the unique isomorphism?

4. • CommentRowNumber4.
   • CommentAuthorYimingXu
   • CommentTimeMay 1st 2023
   • PermaLink
   Author: YimingXu
   Format: MarkdownItexTo me, the proof of replacement of context is just a quotient. I think it is just a matter of when things glues together in a unique way. As I really have to make sure that I understand it correctly. I would like to expand more details of my understanding here. Could someone please check if it is correct? As a minimal working example, say, for each element $u\in U$ there exists up to a unique isomorphism a context $[u,A,B,f:A\to B]$ for the formula $\phi$. Then uniqueness of contexts says for each $u\in U$ there exists a pair of objects $A_u$, $B_u$ and an arrow $f_u:A_u \to B_u$ such that $\phi(u,A_u,B_u,f_u)$ holds. Moreover, for every $A'_u,B'_u,f'_u:A'_u\to B'_u$ such that $\phi(u,A'_u, B'_u,f'_u)$, there exists a unique pair of isomorphisms $i_u:A_u\to A'_u,j_u:B_u\to B'_u$ such that $j_u\circ f_u = f'_u\circ i_u$. By collection of context, we have a regular epi $p:V\to U$ where the regularity here only serves for being able to pullback elements in $U$ into elements in $V$, and a universal context over $V$, consists of a pair of objects $\tilde{A},\tilde{B}$ over $V$ and an arrow $\tilde{f}:\tilde{A}\to \tilde{B}$, such that for each $u\in U$, if we pick any element $v\in V$ such that $p(v) = u$, and we look at the the fibre $\tilde{A}_v$ of $\tilde{A}$, $\tilde{B}_v$ of $\tilde{B}$ over $v$, the universal map $\tilde{f}$ restricts to a map $\tilde{f}_v:\tilde{A}_v \to \tilde{B}_v$. Collection of context says $\phi(p(v), \tilde{A}_v,\tilde{B}_v,\tilde{f}_v)$. The uniqueness then tells us the choice of preimage $v$ in $u$ does not matter, in the sense that we can form a well-defined quotient. Consider the relation on $\tilde{A}$ defined by: (Let $p_A:\tilde{A}\to V,p_B:\tilde{B}\to V$ be the projection of slice category on $V$) $a_1\sim a_2$ iff a. $a_1$ is over the element $v_1\in V$ and $a_2$ is over the element $v_2\in V$, and $p$ identifies $v_1$ and $v_2$ to a same $u$. That is $p(p_A(a_1)) = p(p_A(a_2))$, so $a_1$ and $a_2$ are elements of the $A_u$, $A'_u$ for different choice of the preimage $u$. andalso b.By uniqueness of context, there exists an isomorphism of context, which in particular, includes a map $A_u\to A'_u$, the unique isomorphism moves $a_1$ to $a_2$. Similarly, we can define a relation on $\tilde{B}$. Then $\overline{A}:= \tilde{A}/\sim_A$ and $\overline{B}:= \tilde{B}/\sim_B$ would be the objects of the context over $U$. As for the projection map, the uniqueness condition makes sure that the map $\tilde{A} \to V \to U$ factorizes through this quotient as a well-defined map. To complete the construction of the context we still need an $\overline{f}:\overline{A}\to \overline{B}$. This map is given by: given $[a]\in \overline{A}$, pick a representative $a\in \tilde{A}$, map it to $\tilde{B}$ using $\tilde{f}$ and take the equivalence class $[\tilde{f}(a)] \in \overline{B}$. This map is well-defined because of the uniqueness of context condition.

   To me, the proof of replacement of context is just a quotient. I think it is just a matter of when things glues together in a unique way. As I really have to make sure that I understand it correctly. I would like to expand more details of my understanding here. Could someone please check if it is correct?

   As a minimal working example, say, for each element $u\in U$ there exists up to a unique isomorphism a context $[u,A,B,f:A\to B]$ for the formula $\phi$. Then uniqueness of contexts says for each $u\in U$ there exists a pair of objects $A_u$, $B_u$ and an arrow $f_u:A_u \to B_u$ such that $\phi(u,A_u,B_u,f_u)$ holds. Moreover, for every $A'_u,B'_u,f'_u:A'_u\to B'_u$ such that $\phi(u,A'_u, B'_u,f'_u)$, there exists a unique pair of isomorphisms $i_u:A_u\to A'_u,j_u:B_u\to B'_u$ such that $j_u\circ f_u = f'_u\circ i_u$. By collection of context, we have a regular epi $p:V\to U$ where the regularity here only serves for being able to pullback elements in $U$ into elements in $V$, and a universal context over $V$, consists of a pair of objects $\tilde{A},\tilde{B}$ over $V$ and an arrow $\tilde{f}:\tilde{A}\to \tilde{B}$, such that for each $u\in U$, if we pick any element $v\in V$ such that $p(v) = u$, and we look at the the fibre $\tilde{A}_v$ of $\tilde{A}$, $\tilde{B}_v$ of $\tilde{B}$ over $v$, the universal map $\tilde{f}$ restricts to a map $\tilde{f}_v:\tilde{A}_v \to \tilde{B}_v$. Collection of context says $\phi(p(v), \tilde{A}_v,\tilde{B}_v,\tilde{f}_v)$.

   The uniqueness then tells us the choice of preimage $v$ in $u$ does not matter, in the sense that we can form a well-defined quotient. Consider the relation on $\tilde{A}$ defined by: (Let $p_A:\tilde{A}\to V,p_B:\tilde{B}\to V$ be the projection of slice category on $V$)

   $a_1\sim a_2$ iff

   a. $a_1$ is over the element $v_1\in V$ and $a_2$ is over the element $v_2\in V$, and $p$ identifies $v_1$ and $v_2$ to a same $u$. That is $p(p_A(a_1)) = p(p_A(a_2))$, so $a_1$ and $a_2$ are elements of the $A_u$, $A'_u$ for different choice of the preimage $u$.

   andalso b.By uniqueness of context, there exists an isomorphism of context, which in particular, includes a map $A_u\to A'_u$, the unique isomorphism moves $a_1$ to $a_2$.

   Similarly, we can define a relation on $\tilde{B}$.

   Then $\overline{A}:= \tilde{A}/\sim_A$ and $\overline{B}:= \tilde{B}/\sim_B$ would be the objects of the context over $U$. As for the projection map, the uniqueness condition makes sure that the map $\tilde{A} \to V \to U$ factorizes through this quotient as a well-defined map. To complete the construction of the context we still need an $\overline{f}:\overline{A}\to \overline{B}$. This map is given by: given $[a]\in \overline{A}$, pick a representative $a\in \tilde{A}$, map it to $\tilde{B}$ using $\tilde{f}$ and take the equivalence class $[\tilde{f}(a)] \in \overline{B}$. This map is well-defined because of the uniqueness of context condition.

5. • CommentRowNumber5.
   • CommentAuthorYimingXu
   • CommentTimeMay 1st 2023
   • (edited May 1st 2023)
   • PermaLink
   Author: YimingXu
   Format: MarkdownItexI do not understand the proof in the paper and therefore I suspect that what I said above is problematic. If it is not the case, that is, even if what I said above is true, I still do not see where do we apply replacement of function and equality. I am very confused.

   I do not understand the proof in the paper and therefore I suspect that what I said above is problematic. If it is not the case, that is, even if what I said above is true, I still do not see where do we apply replacement of function and equality. I am very confused.