[Homepage](http://www.cse.chalmers.se/~vezzosi/) ## Selected writings On [[nLab:cubical type theory|cubical]] [[nLab:homotopy type theory]] implemented in the [[nLab:proof assistant]] [[nLab:Cubical Agda]]: * {#VMA19} Andrea Vezzosi, [[nLab:Anders Mörtberg]] and Andreas Abel, _Cubical Agda: A Dependently Typed Programming Language with Univalence and Higher Inductive Types_, 2019 ([pdf](http://www.cs.cmu.edu/~amoertbe/papers/cubicalagda.pdf)) category: people