TY  - RPRT
TI  - Computational Higher Type Theory III: Univalent Universes and Exact Equality
AU  - Carlo Angiuli
AU  - Kuen-Bang Hou
AU  - Robert Harper
PY  - 2017
UR  - https://arxiv.org/abs/1712.01800
ID  - 1712.01800
ER  -