Continuous Functionals of Dependent Types and Equilogical Spaces

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ω).

• Type: Conference
• Year: 2000
• Where: CSL
• Authors: Andrej Bauer, Lars Birkedal
• Keywords: Automated Reasoning, CSL 2000, Dependent Products, Dependent Sums, Realizability Topos