An Induction Principle and Pigeonhole Principles for K-Finite Sets
Logic
2008-02-03 v1
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.
Cite
@article{arxiv.math/9405204,
title = {An Induction Principle and Pigeonhole Principles for K-Finite Sets},
author = {Andreas Blass},
journal= {arXiv preprint arXiv:math/9405204},
year = {2008}
}