Sewon Park: A Dependent Type Theory (under construction) for Multivalued Computation in Computable Analysis

Abstract: Multivalued Computation is essential in computable analysis.
For example, deciding a soft-sign of a real number up to some tolerance parameter is necessarily multivalued.
In this talk, a dependent type theory with a primitive type R for abstract real numbers and a type former M for multivaluedness is devised.
A multivalued real function is, therefore, simply a term, in the type theory, of type R -> M R.
The type former can be applied to sigma types as well, thus that multivalued existences and multivalued disjunctions can be expressed in the type theory.
The type theory has a realizability interpretation in the category of assemblies.