Browsing Bergen Open Research Archive by Author "Escardo, Martin"

Now showing items 1-2 of 2

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