Trying to understand the PCA \(\mathcal{K}_2\) from Van Oosten's Categorical Realizability book, but as far as I can tell, this definition of \(\phi\) doesn't even type check.

Edit: the most charitable reading is to treat the finite sequences as functions, use the definition of <n>*f given on the page, which basically prepends n onto the sequence, and then there are implicit coercions back to numbers using the fixed bijection between finite sequences and numbers...

#realizability

#introduction [en] I am assistant professor in #Saclay (France) in the lab @lmf. Researchwise, I am working in #formal methods and #quantum computing using #type systems, #category theory, #rewriting, #realizability, and text-based and #graphical #languages.

I live in Paris with my family. I commute by #bike when my knees let me do it.

I toot in French and in English.