Blar i Department of Informatics på forfatter "Bezem, Marcus Aloysius"
-
A Model of Type Theory in Cubical Sets
Bezem, Marcus Aloysius; Coquand, Thierry; Huber, Simon (Peer reviewed; Journal article, 2014)We present a model of type theory with dependent product, sum, and identity, in cubical sets. We describe a universe and explain how to transform an equivalence between two types into an equality. We also explain how to ...