Continuous Functionals of Dependent Types and Equilogical Spaces
- 11 May 2000
- Publications
with Lars Birkedal.
Abstract: We show that dependent sums and dependent products of continuous parametrizations on domains with dense, codense, and natural totalities agree with dependent sums and dependent products in equilogical spaces, and thus also in the realizability topos `RT(P(NN))`.
Published in: In Proceedings of Computer Science Logic 2000, Lecture Notes in Computer Science, Vol. 1862, Editors: P.G. Clote, H. Schwichtenberg, Springer, August 2000, pp. 202-216.
Download: dependent_functionals.pdf, dependent_functionals.ps.gz
How to comment on this blog:
At present comments are disabled because the relevant script died.
If you comment on this post on Mastodon and
mention
andrejbauer@mathstodon.xyz, I will
gladly respond.
You are also welcome to contact me directly.