An Induction Principle and Pigeonhole Principles for K-Finite Sets
classification
🧮 math.LO
keywords
principlepigeonholeinductionk-finitesetsbenaboucommentconjectured
read the original 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 Benabou and Loiseau. We also comment on some variants of this pigeonhole principle.
This paper has not been read by Pith yet.
discussion (0)
Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.