10 citations · 11 across the 2 of their papers we have counts for
Showing math.LOShow all
2 papers · 1 filter
math.LO2019★ 1 cited
Canonicity and homotopy canonicity for cubical type theory
Thierry Coquand, Simon Huber, Christian Sattler
Cubical type theory provides a constructive justification of homotopy type theory. A crucial ingredient of cubical type theory is a path lifting operation which is explained comput…
math.LO2017
The univalence axiom in cubical sets
Marc Bezem, Thierry Coquand, Simon Huber
In this note we show that Voevodsky's univalence axiom holds in the model of type theory based on symmetric cubical sets. We will also discuss Swan's construction of the identity t…