category: reference Álvaro Pelayo, [[nLab:Michael Warren|Michael A. Warren]], homotopy type theory and [[Voevodsky's univalent foundations]], [arXiv:1210.5658](http://arxiv.org/abs/1210.5658)