* Paulina Cecchi

Title: Some interactions between words combinatorics and symbolic dynamics.

Abstract: Word combinatorics has been fruitfully used to study several topological and mesure-theoretic properties of dynamical systems, through the analysis of suitably chosen symbolic dynamical systems. In this talk, we will introduce some notions of symbolic dynamics and present some examples which illustrate how word combinatorics can be used as a tool to solve questions arising from this branch of mathematics.

*

* Antoine Allioux

Title: The curse of Martin-Löf identity type

Abstract: The identity type of Intuitionistic Type Theory (ITT) endows types with a structure of infinity-groupoid. This higher structure follows from the fact that the Uniqueness of Identity Proof (UIP) is not derivable in ITT. Homotopy Type Theory (HoTT) takes advantage of this observation by enriching ITT with new principles which are coherent with this interpretation, namely the Univalence Axiom and the Higher Inductive Types (HITs).

HITs are a generalization of inductive types which allow, in addition to create regular inhabitants of an inductive type, to postulate identities between them as well as identities between these identities, and that ad infinitum. It is then tempting to try to present mathematical structures using these new types like one would do in mathematics using generators and relations.

However, problems quickly arise as soon as one needs a strict equality. Indeed, the identity type expresses a weak equality leading to the usual coherence problems. Trying to solve these naively, we run into the problem of having to define an infinite sequence of coherence data.

If HoTT is to be a credible foundation of mathematics, the question of formalizing structures which need a strict equality is crucial. The answer to this question rests, in part, upon our achievement to either present these structures differently in the existing theory or to enrich it so that it becomes tractable to express them.

*