Constructive mathematics and semiclassical principles in homotopy type theory
» Apply now PDF Show all positions
Abstract
The topic of this PhD project is homotopy type theory, a logical framework for mathematics, particularly suited for homotopy theory and higher category theory. This PhD project investigates the expressivity of homotopy type theory as a foundational system for the development of constructive mathematics, especially the interaction between higher inductive and coinductive types with semiclassical principles.
| Research field: |
Information and communication technology |
|---|---|
| Supervisors: |
Dr. Tarmo Uustalu Dr. Niccoló Veltri |
| Availability: | This position is available. |
| Offered by: |
School of Information Technologies Department of Software Science |
| Application deadline: | Applications are accepted between June 01, 2022 00:00 and June 30, 2022 23:59 (Europe/Zurich) |
Description
This PhD project investigates the relationship between (i) new features of homotopy type theory, in particular higher inductive types, but also new principles such as univalence and propositional resizing, (ii) standard datatypes used in proof assistants for the representation of infinite objects, such as coinductive types, (iii) semiclassical principles employed/rejected by different trends of constructive mathematics, such as variants of the axiom of choice, bar induction and weak versions of the law of excluded middle. This three notions often interact when one tries to construct the quotient (a higher inductive type) of an infinite structure (an element of a coinductive types), an activity practically motivated by denotational semantics of programming languages. The resulting object often fails to behave as expected, e.g. Capretta's delay monad quotiented by weak bisimilarity is not a monad, unless one postulates the validity of semiclassical principles such as countable choice, or assumes as primitive the expressive scheme of higher induction-induction. The relationship between (i)-(iii) will be studied both internally in homotopy type theory but also externally in simplicial/cubical set models.
Responsibilities and tasks:
The student’s primary responsibility is research on this PhD project. The student may have contribute to the teaching activities of the lab as a course assistant.
Qualifications:
- Candidates must have a MSc degree in mathematics or computer science.
- The applicants should fulfill the following requirements:
- The successful candidate is knowledgeable in at least one and interested in all of the following: type theory, category theory, constructive mathematics, logic, certified programming.