Predictive type universes and primitive recursion
- 10 December 2002
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
- p. 173-184
- https://doi.org/10.1109/lics.1991.151642
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 omega is constructed.Keywords
This publication has 5 references indexed in Scilit:
- Constructive Mathematics and Computer ProgrammingPublished by Elsevier ,2014
- Generalised algebraic theories and contextual categoriesPublished by Elsevier ,2003
- A categorical semantics of constructionsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2003
- Locally cartesian closed categories and type theoryMathematical Proceedings of the Cambridge Philosophical Society, 1984
- The algebraic specification of abstract data typesActa Informatica, 1978