We make a systematic study of filtrations of a free group F defined as products of powers of the lower central series of F. Under some assumptions on the exponents, we characterize these filtrations in terms of the group algebra, the Magnus algebra of non-commutative power series, and linear representations by upper-triangular unipotent matrices. These characterizations generalize classical results of Grun, Magnus, Witt, and Zassenhaus from the 1930's, as well as later results on the lower p-central filtration and the p-Zassenhaus filtrations. We derive alternative recursive definitions of such filtrations, extending results of Lazard.

Around ten years ago, it was discovered that Martin-Lof's Intensional Type Theory - a logical system designed in the 1970's as a more constructive and computational alternative to ZFC-style foundations - admits quite unexpected interpretations in simplicial sets and other homotopy-theoretic settings. More than this: under this interpretation, the logic turned out to be remarkably powerful for expressing and reasoning with standard homotopy-theoretic properties and constructions, in very elementary ways. This connection has since proved extremely fruitful, and the resulting programme of work has become known as *Homotopy Type Theory* or *Univalent Foundations*.

In this talk, I will give a general introduction to type theory, and a survey of the recent homotopically-influenced developments - in particular, of the connections with $\infty$-toposes in the sense of Rezk/Lurie, for which it is hoped that type theory can provide an "internal language", in a certain precise sense.

We make a systematic study of filtrations of a free group F defined as products of powers of the lower central series of F. Under some assumptions on the exponents, we characterize these filtrations in terms of the group algebra, the Magnus algebra of non-commutative power series, and linear representations by upper-triangular unipotent matrices. These characterizations generalize classical results of Grun, Magnus, Witt, and Zassenhaus from the 1930's, as well as later results on the lower p-central filtration and the p-Zassenhaus filtrations. We derive alternative recursive definitions of such filtrations, extending results of Lazard.