An Induction Principle and Pigeonhole Principles for K-Finite Sets

2026-07-072026-07-07http://salesiana.dossiersoluciones.com/handle/123456789/152907We 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.LogicAn Induction Principle and Pigeonhole Principles for K-Finite Setstext