University of Birmingham > Talks@bham > Lab Lunch > Analysis in univalent type theory

Analysis in univalent type theory

Add to your list(s) Download to your calendar using vCal

If you have a question about this talk, please contact Dr Steve Vickers.

Practice talk for the Oberseminar Mathematische Logik in M√ľnchen at Chuangjie’s group.

It is not possible to exhibit information about real numbers such as Dedekind reals or (quotiented) Cauchy reals (as opposed to Bishop-style Cauchy reals), because, for example, there are no non-constant functions into observable types such as the booleans or the integers. We overcome this by considering real numbers that have additional structure, which we call strong locatedness. With this structure, it is possible, for instance, to construct a signed-digit representation or a Cauchy approximation. Such constructions are reminiscent of computable analysis. However, the main point is that instead of working with a notion of computability, we simply work constructively to extract observational information.

This talk is part of the Lab Lunch series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.

 

Talks@bham, University of Birmingham. Contact Us | Help and Documentation | Privacy and Publicity.
talks@bham is based on talks.cam from the University of Cambridge.