Computational Higher Type Theory III: Univalent Universes and Exact Equality

Carlo Angiuli, Kuen-Bang Hou, Robert Harper

This is the third in a series of papers extending Martin-Löf's meaning explanations of dependent type theory to a Cartesian cubical realizability framework that accounts for higher…