Jonas will present the following paper and lead the discussion.

Cyril Cohen, Thierry Coquand, Simon Huber, and Anders Mörtberg. 2016. Cubical Type Theory: a constructive interpretation of the univalence axiom. arXiv (2016). DOI:https://doi.org/10.48550/arxiv.1611.02108