Article contents
An induction principle and pigeonhole principles for K-finite sets
Published online by Cambridge University Press: 12 March 2014
Abstract
We establish a course-of-values induction principle for K-finite sets in intuitionistic type theory. Using this principle, we prove a pigeonhole principle conjectured by Bénabou and Loiseau. We also comment on some variants of this pigeonhole principle.
Keywords
- Type
- Research Article
- Information
- Copyright
- Copyright © Association for Symbolic Logic 1995
References
REFERENCES
- 2
- Cited by