| Popis: |
The present paper investigates the use of impredicative methods for the construction of inductive types in homotopy type theory. Inductive types have been constructed impredicatively in other systems of type theory in the past, but these fail to have the correct rules. Using new methods, the paper shows how to repair these prior constructions, and extend the impredicative methodology to include also the newly discovered higher inductive types that form the basis of the recent applications in homotopy theory. This present work refines and extends the traditional logistic approach to foundations of mathematics to encompass both arithmetic and geometry in a comprehensive logistic system that also admits a computational implementation on modern computing machines. The connection to the idea of mathesis universalis is thus quite direct. |
