# Homotopical inductive types

Lead Research Organisation:
University of Leeds

Department Name: Pure Mathematics

### Abstract

Over the past few years, new surprising connections have emerged between two traditionally distant areas of mathematics: mathematical logic (which is generally concerned with the study of the forms of reasoning used in mathematics) and homotopy theory (which is interested in understanding and classifying various notions of space). These connections are useful because they provide a clear

geometric intuition that helps us to work with a class of logical systems, known as type theories. On that basis, the Fields medallist Vladimir Voevodsky has formulated an ambitious research programme, called the Univalent Foundations of Mathematics programme, that seeks to develop a new foundations of mathematics on the basis of type theories that include new axioms motivated by homotopy theory.

The proposed research seeks to advance our understanding of the type theories proposed by Voevodsky in order to develop the Univalent Foundations programme. Our first goal is to understand better the relationship between the type theories introduced by Voevodsky and axiomatic set theories, which represent the more traditional approach to foundations of mathematics. In particular, we want to clarify the logical status of the Univalence Axiom, a new axiom which allows us to treat objects that share all structural properties as equal. Furthermore, we wish to gain further insight into a variation, again motivated by homotopy theory, over the standard way of defining types.

geometric intuition that helps us to work with a class of logical systems, known as type theories. On that basis, the Fields medallist Vladimir Voevodsky has formulated an ambitious research programme, called the Univalent Foundations of Mathematics programme, that seeks to develop a new foundations of mathematics on the basis of type theories that include new axioms motivated by homotopy theory.

The proposed research seeks to advance our understanding of the type theories proposed by Voevodsky in order to develop the Univalent Foundations programme. Our first goal is to understand better the relationship between the type theories introduced by Voevodsky and axiomatic set theories, which represent the more traditional approach to foundations of mathematics. In particular, we want to clarify the logical status of the Univalence Axiom, a new axiom which allows us to treat objects that share all structural properties as equal. Furthermore, we wish to gain further insight into a variation, again motivated by homotopy theory, over the standard way of defining types.

### Planned Impact

The modern world relies in an essential way on computer systems to run important tasks in a variety of areas: from finance and medicine to transport and energy. When computer systems are used in safety-critical applications (such as controlling the functioning of a nuclear power station or coordinating the signal system of a train network), it is essential that their correctness is established without doubt, and not merely indicated by tests.

One successful approach to the verification of software correctness has been to develop integrated software systems, known as proof assistants, in which it is possible to write computer programs, specify requirements, and formally prove that these requirements hold. Thus, these systems give us a way of creating correct-by-construction programs, which is beneficial also in economic terms since it eliminates the difficult process of debugging. The development of proof assistants involved a combination of ideas of mathematical logic and computer science, in a way that is reminiscent of the very origin of computer programming. Indeed, proof assistants are also used in the formalisation of mathematical proofs, so as to guarantee their correctness.

The proposed research focuses on logical systems, known as type theories, which are at the core of some of the most powerful proof assistants (such as the Coq system). In particular, we seek to advance our understanding of a new class of type theories which have been recently formulated by the Fields medallist Vladimir Voevodsky, thanks to the discovery of surprising connections between

mathematical logic and homotopy theory (an area of mathematics that studies general notions of space).

Our proposed research will benefit directly the academic communities working in mathematical logic, homotopy theory and higher-dimensional category theory by improving our understanding of this new class of type theories and of the connections between these subjects. Our work is likely to impact also the ongoing design of new proof assistants based on these new type theories, since it aims to obtain precise information on their expressive power. These new proof assistants, in turn, will benefit society in general by facilitating the creation of correct-by-construction computer programs.

One successful approach to the verification of software correctness has been to develop integrated software systems, known as proof assistants, in which it is possible to write computer programs, specify requirements, and formally prove that these requirements hold. Thus, these systems give us a way of creating correct-by-construction programs, which is beneficial also in economic terms since it eliminates the difficult process of debugging. The development of proof assistants involved a combination of ideas of mathematical logic and computer science, in a way that is reminiscent of the very origin of computer programming. Indeed, proof assistants are also used in the formalisation of mathematical proofs, so as to guarantee their correctness.

The proposed research focuses on logical systems, known as type theories, which are at the core of some of the most powerful proof assistants (such as the Coq system). In particular, we seek to advance our understanding of a new class of type theories which have been recently formulated by the Fields medallist Vladimir Voevodsky, thanks to the discovery of surprising connections between

mathematical logic and homotopy theory (an area of mathematics that studies general notions of space).

Our proposed research will benefit directly the academic communities working in mathematical logic, homotopy theory and higher-dimensional category theory by improving our understanding of this new class of type theories and of the connections between these subjects. Our work is likely to impact also the ongoing design of new proof assistants based on these new type theories, since it aims to obtain precise information on their expressive power. These new proof assistants, in turn, will benefit society in general by facilitating the creation of correct-by-construction computer programs.

## People |
## ORCID iD |

Michael Rathjen (Principal Investigator) | |

Nicola Gambino (Researcher) |

### Publications

Cook J
(2016)

*Advances in Proof Theory*
Cook J
(2016)

*Classifying the Provably Total set Functions of KP and KP(P)*in The IfCoLog Journal of Logics and their Applications
Dihoum E
(2019)

*Preservation of choice principles under realizability*in Logic Journal of the IGPL
Gambino Nicola
(2014)

*On operads, bimodules and analytic functors*in arXiv e-prints
RATHJEN M
(2016)

*INDEFINITENESS IN SEMI-INTUITIONISTIC SET THEORIES: ON A CONJECTURE OF FEFERMAN*in The Journal of Symbolic Logic
Rathjen M
(2017)

*Feferman on Foundations*
Rathjen M
(2017)

*Long Sequences of Descending Theories and other Miscellenia on Slow Consistency*in IfCoLog Journal of Logics and their Applications
Rathjen M
(2016)

*Concepts of Proof in Mathematics, Philosophy, and Computer Science*
Rathjen M
(2019)

*The scope of Feferman's semi-intuitionistic set theories and his second conjecture*in Indagationes Mathematicae
Rathjen M

*Power Kripke-Platek set theory and the axiom of choice*in Journal of Logic and ComputationDescription | We have developed technical tools for dealing with infinitary intuitionistic derivations and rextracting computational information from them in the presence of strong axioms such as Powerset and Exponentiation and used them to determine the strength of type theories with the type of propositions. We also proved several of Feferman's conjectures pertaining to the indeterminacy of iconic set-theoretic statements in semi-intuitionistic set theories. |

Exploitation Route | They will provide answers concerning the strength of current proof assistants. |

Sectors | Creative Economy |

Description | Results about the indefinitness of the continuum problem in semi-intuitionistic set theories have stirred a lot of interest in set theory and the philosophy of mathematics. |

First Year Of Impact | 2014 |

Sector | Other |

Impact Types | Cultural |