I can never remember the formula for the closure operator 𝑗 : 𝖯𝗋𝗈𝗉 → 𝖯𝗋𝗈𝗉 forcing a predicate 𝑃 : 𝐴 → 𝖯𝗋𝗈𝗉 to be true. It is this:
[j(q) = \forall r \in \mathsf{Prop} ., (q \Rightarrow r) \Rightarrow (\forall x \in A., ((P,x \Rightarrow r) \Rightarrow r)) \Rightarrow r]
Would you remember it? I first saw it as a PhD student in a talk by Jaap van Oosten, and had a “wtf” sort of reaction to it, which I still do. I think it shaped my mental image of Jaap (in a good way).
Anyhow, every once in a while I spend 15 minutes looking for it in Jaap's book on realizability, after which I remember it's also in Martin Hyland's paper on the effective topos. The paper is very old, but someone converted it to PDF and it's online, and the formula is in there (see pasted image).
In the hope that the next time I need the formula I will remember I formalized it in Coq (because Agda is predicative and Lean classical), here is the gist: https://gist.github.com/andrejbauer/4f984149fc6694efdbe61b0f9dc55999
All this is doable in HoTT, see @aws's paper on Oracle modalities https://arxiv.org/abs/2406.05818, which has much more than just the homotopy-theoretic construction of the closure operator.
A task worthy of a social network: tell a a story about what the formula is doing. It should explain why (r \mapsto \forall x \in A., (P,x \Rightarrow r)) is the wrong answer.
=> More informations about this toot | View the thread | More toots from andrejbauer@mathstodon.xyz
=> View aws@mathstodon.xyz profile
text/geminiThis content has been proxied by September (3851b).