The seminar below is held as a part of JSPS Core-to-Core Program,

A. Advanced Research Networks, and EU FP7 Marie Curie Actions IRSES project CORCON. (http://www.jaist.ac.jp/logic/ja/core2core, https://corcon.net/)

Wednesday 28 September, 2016, 15:20-17:00 in JAIST, Collaboration room 7 (I-56)

(Access: http://www.jaist.ac.jp/english/location/access.html)

**Dr Chuangjie Xu** (Ludwig-Maximilians-Universität München) Continuity in Type Theory

If all functions (N -> N) -> N are continuous then 0 = 1. We

establish this in intuitionistic type theory, with existence in the

formulation of continuity expressed as a Sigma-type via the

Curry-Howard interpretation. But with an intuitionistic notion of

anonymous existence, defined as the propositional truncation of

Sigma, it is consistent that all such functions are continuous. On

the other hand, any of these two intuitionistic conceptions of

existence give the same, consistent, notion of uniform continuity

for functions (N -> 2) -> N. Moreover, we constructively develop a

model of uniform continuity and implemented it within type theory

using Agda.