Blar i Department of Informatics på forfatter "Coquand, Thierry"
-
Loop-checking and the uniform word problem for join-semilattices with an inflationary endomorphism
Bezem, Marc; Coquand, Thierry (Journal article; Peer reviewed, 2022)We solve in polynomial time two decision problems that occur in type checking when typings depend on universe level constraints. -
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 (Journal article; 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 ... -
On generalized algebraic theories and categories with families
Bezem, Marc; Coquand, Thierry; Dybjer, Peter; Escardo, Martin (Journal article; Peer reviewed, 2021)We give a syntax independent formulation of finitely presented generalized algebraic theories as initial objects in categories of categories with families (cwfs) with extra structure. To this end, we simultaneously define ...