10 citations · 11 across the 2 of their papers we have counts for
Showing cs.LOShow all
3 papers · 1 filter
cs.LO2018
On Higher Inductive Types in Cubical Type Theory
Thierry Coquand, Simon Huber, Anders Mörtberg
Cubical type theory provides a constructive justification to certain aspects of homotopy type theory such as Voevodsky's univalence axiom. This makes many extensionality principles…
cs.LO2016★ 10 cited
Cubical Type Theory: a constructive interpretation of the univalence axiom
Cyril Cohen, Thierry Coquand, Simon Huber +1
This paper presents a type theory in which it is possible to directly manipulate -dimensional cubes (points, lines, squares, cubes, etc.) based on an interpretation of dependent…
cs.LO2016
Canonicity for Cubical Type Theory
Simon Huber
Cubical type theory is an extension of Martin-Löf type theory recently proposed by Cohen, Coquand, Mörtberg and the author which allows for direct manipulation of -dimensional c…