Post #2777171
2026-05-22 08:21 UTC
Replies (1)
-
@Paul_Taylor@mathstodon.xyz 2026-05-22 09:46
@mc@mathstodon.xyz Lawvere said "quantifiers are adjoint to substitution". No, they are adjoint to weakening: see (my thesis and) the last chapter of my book "Practical Foundations of Mathematics" (CUP 1999). The difference between set theory and topology is that the former has all quantifiers in this sense, but the latter has universal quantifiers over compact spaces and existential ones over overt ones: see my work on Abstract Stone Duality. My (thesis and) book also treated display maps, which are the semantics of weakening by types; I am currently working on completeness for that, which I messed up in my book, so if you are thinking about these things too I would appreciate some help checking the details in my proof.