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” 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:AB} over U, given that for each u:1U, there exists a context X,Y,f:XY such that ϕ(u,X,Y,f:XY), to unwind this layer by layer, we can write X(Yf:XY.ϕ(u,X,Y,f)). We set ψ(u,X):=Yf:XY.ϕ(u,X,Y,f), then by collection of sets, for each u:1U, there exists a set X such that ψ(u,X). Then we get a regular epi p:VU and a pA:AV such that for each v:1V, ψ(pv,v*A). And for the next layer, we use the fact that for each v:1V, we have Y.(f.ϕ(pv,v*A,Y,f:v*AY)) and set φ(v,Y):=f.ϕ(pv,v*A,Y,f:v*AY), then by collection of sets we have a regular epi q:WV and a fB:BW, such that for all w:1W, we have f.ϕ(pqw,w*q*A,f:w*q*AB). Also, the composition pq is a regular epi WU. 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×UV, 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*Θ in Set/V×UV

    Over each element z:1V×UV, 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 uU there exists up to a unique isomorphism a context [u,A,B,f:AB] for the formula ϕ. Then uniqueness of contexts says for each uU there exists a pair of objects Au, Bu and an arrow fu:AuBu such that ϕ(u,Au,Bu,fu) holds. Moreover, for every Au,Bu,fu:AuBu such that ϕ(u,Au,Bu,fu), there exists a unique pair of isomorphisms iu:AuAu,ju:BuBu such that jufu=fuiu. By collection of context, we have a regular epi p:VU 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 ˜A,˜B over V and an arrow ˜f:˜A˜B, such that for each uU, if we pick any element vV such that p(v)=u, and we look at the the fibre ˜Av of ˜A, ˜Bv of ˜B over v, the universal map ˜f restricts to a map ˜fv:˜Av˜Bv. Collection of context says ϕ(p(v),˜Av,˜Bv,˜fv).

    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 ˜A defined by: (Let pA:˜AV,pB:˜BV be the projection of slice category on V)

    a1a2 iff

    a. a1 is over the element v1V and a2 is over the element v2V, and p identifies v1 and v2 to a same u. That is p(pA(a1))=p(pA(a2)), so a1 and a2 are elements of the Au, Au 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 AuAu, the unique isomorphism moves a1 to a2.

    Similarly, we can define a relation on ˜B.

    Then ˉA:=˜A/A and ˉB:=˜B/B would be the objects of the context over U. As for the projection map, the uniqueness condition makes sure that the map ˜AVU factorizes through this quotient as a well-defined map. To complete the construction of the context we still need an ˉf:ˉAˉB. This map is given by: given [a]ˉA, pick a representative a˜A, map it to ˜B using ˜f and take the equivalence class [˜f(a)]ˉ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.