Blar i Bergen Open Research Archive på forfatter "Bezem, Marc"

Viser treff 1-5 av 5

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

    • Type Theory with Explicit Universe Polymorphism 

      Bezem, Marc; Coquand, Thierry; Dybjer, Peter; Escardo, Martin (Journal article; Peer reviewed, 2023)
      The aim of this paper is to refine and extend proposals by Sozeau and Tabareau and by Voevodsky for universe polymorphism in type theory. In those systems judgments can depend on explicit constraints between universe levels. ...