Logic in Computer Science (LICS 1991)

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

Authors: Nax Paul 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 Paul Mendler},
    title = 	 {Predictive type universes and primitive recursion},
    booktitle =  {Proceedings of the Sixth Annual IEEE Symp. on Logic in Computer Science, {LICS} 1991},
    year =	 1991,
    editor =	 {Giles Kahn},
    month =	 {July}, 
    pages =      {173--184},
    location =   {Amsterdam, The Netherlands}, 
    publisher =	 {IEEE Computer Society Press}
  }