Not signed in (Sign In)

Not signed in

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

  • Sign in using OpenID

Discussion Tag Cloud

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).
    • CommentRowNumber1.
    • CommentAuthorYimingXu
    • CommentTimeApr 12th 2023

    Hi, all.

    I am a bit confused by the proofs in “comparing material and structural set theories”

    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:AB}\{X,Y,f:A\to B\} over UU, given that for each u:1Uu:1\to U, there exists a context X,Y,f:XYX,Y, f:X\to Y such that ϕ(u,X,Y,f:XY)\phi(u,X,Y,f:X\to Y), to unwind this layer by layer, we can write X(Yf:XY.ϕ(u,X,Y,f))\exists X (\exists Y \;\exists f:X\to Y. \phi(u,X,Y,f)). We set ψ(u,X):=Yf:XY.ϕ(u,X,Y,f)\psi(u,X):= \exists Y \;\exists f:X\to Y. \phi(u,X,Y,f), then by collection of sets, for each u:1Uu:1\to U, there exists a set XX such that ψ(u,X)\psi(u,X). Then we get a regular epi p:VUp:V\to U and a p A:AVp_A:A\to V such that for each v:1Vv:1\to V, ψ(pv,v *A)\psi(pv, v^*A). And for the next layer, we use the fact that for each v:1Vv:1\to V, we have Y.(f.ϕ(pv,v *A,Y,f:v *AY))\exists Y.(\exists f.\phi(pv,v^*A,Y,f:v^*A \to Y)) and set φ(v,Y):=f.ϕ(pv,v *A,Y,f:v *AY)\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:WVq:W\to V and a f B:BWf_B:B\to W, such that for all w:1Ww:1\to W, we have f.ϕ(pqw,w *q *A,f:w *q *AB)\exists f. \phi(pqw,w^*q^*A,f:w^*q^*A \to B). Also, the composition pqp\circ q is a regular epi WUW\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.

    • CommentRowNumber2.
    • CommentAuthorMike Shulman
    • CommentTimeApr 17th 2023

    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.

    • CommentRowNumber3.
    • CommentAuthorYimingXu
    • CommentTimeApr 27th 2023
    • (edited Apr 27th 2023)

    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:1V× UVz : 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 *Θs *Θr^*\Theta \cong s^*\Theta in Set/V× UVSet/V \times_U V

    Over each element z:1V× UVz: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?

    • CommentRowNumber4.
    • CommentAuthorYimingXu
    • CommentTimeMay 1st 2023

    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 uUu\in U there exists up to a unique isomorphism a context [u,A,B,f:AB][u,A,B,f:A\to B] for the formula ϕ\phi. Then uniqueness of contexts says for each uUu\in U there exists a pair of objects A uA_u, B uB_u and an arrow f u:A uB uf_u:A_u \to B_u such that ϕ(u,A u,B u,f u)\phi(u,A_u,B_u,f_u) holds. Moreover, for every A u,B u,f u:A uB uA'_u,B'_u,f'_u:A'_u\to B'_u such that ϕ(u,A u,B u,f u)\phi(u,A'_u, B'_u,f'_u), there exists a unique pair of isomorphisms i u:A uA u,j u:B uB ui_u:A_u\to A'_u,j_u:B_u\to B'_u such that j uf u=f ui uj_u\circ f_u = f'_u\circ i_u. By collection of context, we have a regular epi p:VUp:V\to U where the regularity here only serves for being able to pullback elements in UU into elements in VV, and a universal context over VV, consists of a pair of objects A˜,B˜\tilde{A},\tilde{B} over VV and an arrow f˜:A˜B˜\tilde{f}:\tilde{A}\to \tilde{B}, such that for each uUu\in U, if we pick any element vVv\in V such that p(v)=up(v) = u, and we look at the the fibre A˜ v\tilde{A}_v of A˜\tilde{A}, B˜ v\tilde{B}_v of B˜\tilde{B} over vv, the universal map f˜\tilde{f} restricts to a map f˜ v:A˜ vB˜ v\tilde{f}_v:\tilde{A}_v \to \tilde{B}_v. Collection of context says ϕ(p(v),A˜ v,B˜ v,f˜ v)\phi(p(v), \tilde{A}_v,\tilde{B}_v,\tilde{f}_v).

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

    a 1a 2a_1\sim a_2 iff

    a. a 1a_1 is over the element v 1Vv_1\in V and a 2a_2 is over the element v 2Vv_2\in V, and pp identifies v 1v_1 and v 2v_2 to a same uu. That is p(p A(a 1))=p(p A(a 2))p(p_A(a_1)) = p(p_A(a_2)), so a 1a_1 and a 2a_2 are elements of the A uA_u, A uA'_u for different choice of the preimage uu.

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

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

    Then A¯:=A˜/ A\overline{A}:= \tilde{A}/\sim_A and B¯:=B˜/ B\overline{B}:= \tilde{B}/\sim_B would be the objects of the context over UU. As for the projection map, the uniqueness condition makes sure that the map A˜VU\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 f¯:A¯B¯\overline{f}:\overline{A}\to \overline{B}. This map is given by: given [a]A¯[a]\in \overline{A}, pick a representative aA˜a\in \tilde{A}, map it to B˜\tilde{B} using f˜\tilde{f} and take the equivalence class [f˜(a)]B¯[\tilde{f}(a)] \in \overline{B}. This map is well-defined because of the uniqueness of context condition.

    • CommentRowNumber5.
    • CommentAuthorYimingXu
    • CommentTimeMay 1st 2023
    • (edited May 1st 2023)

    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.