Rencontre,
Oct. 20, 2022

## Martin Baillon (Gallinette, LS2N), Gardening with the Pythia, A model of continuity in a dependent setting

### Schedule

- Oct. 20, 2022, 14:00 - 15:00

### Abstract

We generalize to a rich dependent type theory a proof originally developed by Escardó that all System T functionals are continuous. It relies on the definition of a syntactic model of Baclofen Type Theory, a type theory where dependent elimination must be strict, into the Calculus of Inductive Constructions.

The model is given by three translations: the axiom translation, that adds an oracle to the context; the branching translation, based on the dialogue monad, turning every type into a tree; and finally, a layer of algebraic binary parametricity, binding together the two translations. In the resulting type theory, every function f : (N → N) → N is externally continuous.