Higher Universal Algebra in Type Theory

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

• Eric Finster, INRIA, Paris
• Tuesday 22 January 2019, 15:00-16:00
• Computer Science, 245.

If you have a question about this talk, please contact Jamie Vicary.

I will describe recent progress on understanding higher algebraic structures in dependent type theory. In particular, I show how one can define a coherent version of polynomial monad, whose special cases include definitions of $(\infty,1)$-category and $\infty$-groupoid. I will also explain how these techniques yield a definition of simplicial type, discuss progress on formalization and formulate a number of conjectures aimed testing the definition’s suitability.

This talk is part of the Theoretical computer science seminar series.

This talk is included in these lists:

• Computer Science Departmental Series
• Computer Science Distinguished Seminars
• Computer Science, 245
• Theoretical computer science seminar
• computer sience

Note that ex-directory lists are not shown.