• 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 ...
    • Non-Constructivity in Kan Simplicial Sets 

      Bezem, Marc; Coquand, Thierry; Parmann, Erik (Conference object; Peer reviewed, 2015)
      We give an analysis of the non-constructivity of the following basic result: if X and Y are simplicial sets and Y has the Kan extension property, then Y X also has the Kan extension property. By means of Kripke countermodels ...