Abstract
Having the type of all types in a type system results in paradoxes like Russel’s paradox. Therefore type theories like predicative calculus of inductive constructions (pCIC) – the logic of the Coq proof assistant – have a hierarchy of types
, ..., where
, .... In a cumulative type system, e.g., pCIC, for a term
such that
we also have that
. The system pCIC has recently been extended to support universe polymorphism, i.e., definitions can be parametrized by universe levels. This extension does not support cumulativity for inductive types. For example, we do not have that a pair of types at levels i and j is also considered a pair of types at levels \(i + 1\) and \(j + 1\).
In this paper, we discuss our on-going research on making inductive types cumulative in the pCIC. Having inductive types be cumulative alleviates some problems that occur while working with large inductive types, e.g., the category of small categories, in pCIC.
We present the pCuIC system which adds cumulativity for inductive types to pCIC and briefly discuss some of its properties and possible extensions. We, in addition, give a justification for the introduced cumulativity relation for inductive types.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
Here, smallness and largeness are to be understood as relative to universe levels.
- 2.
Subject to side constraints on universe levels, e.g., \(k, l<i\).
References
Coquand, T., Paulin, C.: Inductively defined types. In: COLOG 1988, Proceedings of International Conference on Computer Logic, Tallinn, USSR, pp. 50–66, December 1988
Luo, Z.: An Extended Calculus of Constructions. Ph.D. thesis, University of Edinbrugh, Department of Computer Science, June 1990
The Coq development team: Coq 8.2 Reference Manual. Inria (2008)
Paulin-Mohring, C.: Inductive definitions in the system Coq - rules and properties. In: Proceedings of International Conference on Typed Lambda Calculi and Applications, TLCA 1993, Utrecht, The Netherlands, pp. 328–345, March 1993
Paulin-Mohring, C.: Introduction to the Calculus of Inductive Constructions, November 2014. https://hal.inria.fr/hal-01094195
Sozeau, M., Tabareau, N.: Universe polymorphism in Coq. In: Klein, G., Gamboa, R. (eds.) ITP 2014. LNCS, vol. 8558, pp. 499–514. Springer, Heidelberg (2014)
Timany, A., Jacobs, B.: Category theory in Coq 8.5. CoRR abs/1505.06430 (2015), http://www.arxiv.org/abs/1505.06430, accepted for a presentation at the 7th Coq workshop, Sophia Antipolis, France on 26 June 2015
Timany, A., Jacobs, B.: First Steps Towards Cumulative Inductive Types in CIC: Extended Version. Technical Report CW684, iMinds-Distrinet, KU Leuven, March 2015. http://www2.cs.kuleuven.be/publicaties/rapporten/cw/CW684.abs.html
Acknowledgements
This work was funded by EU FP7 FET-Open project ADVENT under grant number 308830.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer International Publishing Switzerland
About this paper
Cite this paper
Timany, A., Jacobs, B. (2015). First Steps Towards Cumulative Inductive Types in CIC. In: Leucker, M., Rueda, C., Valencia, F. (eds) Theoretical Aspects of Computing - ICTAC 2015. ICTAC 2015. Lecture Notes in Computer Science(), vol 9399. Springer, Cham. https://doi.org/10.1007/978-3-319-25150-9_36
Download citation
DOI: https://doi.org/10.1007/978-3-319-25150-9_36
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-25149-3
Online ISBN: 978-3-319-25150-9
eBook Packages: Computer ScienceComputer Science (R0)