36 citations · 143 across the 40 of their papers we have counts for
Showing 2018Show all
3 papers · 1 filter
math.AC2018
Résolutions libres finies. Méthodes constructives
Thierry Coquand, Henri Lombardi, Claude Quitté +1
In this memoir, we give a completely constructive version of the celebrate book 'Finite Free Resolutions' by Northcott, and of some other results related to the depth à la Hochster…
cs.PL2018
Canonicity and normalisation for Dependent Type Theory
Thierry Coquand
We show canonicity and normalization for dependent type theory with a cumulative sequence of universes and a type of Boolean. The argument follows the usual notion of reducibility,…
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…