Blar i Department of Informatics på forfatter "Bezem, Marc"
-
Construction of the circle in UniMath
Bezem, Marc; Buchholtz, Ulrik; Grayson, Daniel R.; Shulman, Michael (Journal article; Peer reviewed, 2021)We show that the type TZ of Z-torsors has the dependent universal property of the circle, which characterizes it up to a unique homotopy equivalence. The construction uses Voevodsky’s Univalence Axiom and propositional ... -
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. -
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 ...