Paper: Predictive type universes and primitive recursion (at LICS 1991)

Authors: Nax P. Mendler

Abstract

A category-theoretic explanation of predicative type universes and primitive recursion on them is given. Categories with display maps (cdm) (with canonical pullbacks) are used to model families. A slight generalization of an algebra, called an I-algebra, is given. Primitive recursion is defined, and the general definition of primitive recursion on a cdm which can justify the elimination rules for all the usual inductively defined datatypes, including universes, as an instance, is given. It is shown how operations may be reflected, allowing an I-algebra to be closed under type-forming operations. Universe hierarchies are built: an externally constructed one, and then a large type universe, itself closed under universe construction, in which universe hierarchies can be internally constructed. As an example, a hierarchy up to ω is constructed

BibTeX

  @InProceedings{Mendler-Predictivetypeunive,
    author = 	 {Nax P. Mendler},
    title = 	 {Predictive type universes and primitive recursion},
    booktitle =  {Proceedings of the Sixth Annual IEEE Symposium on Logic in Computer Science (LICS 1991)},
    year =	 {1991},
    month =	 {July}, 
    pages =      {173--184},
    location =   {Amsterdam, The Netherlands}, 
    publisher =	 {IEEE Computer Society Press}
  }