• 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 ...