| EPSRC Reference: |
EP/K023128/1 |
| Title: |
Homotopical inductive types |
| Principal Investigator: |
Rathjen, Professor M |
| Other Investigators: |
|
| Researcher Co-Investigators: |
|
| Project Partners: |
|
| Department: |
Pure Mathematics |
| Organisation: |
University of Leeds |
| Scheme: |
Standard Research |
| Starts: |
01 May 2013 |
Ends: |
27 June 2016 |
Value (£): |
283,814
|
| EPSRC Research Topic Classifications: |
| Algebra & Geometry |
Fundamentals of Computing |
| Logic & Combinatorics |
|
|
| EPSRC Industrial Sector Classifications: |
|
| Related Grants: |
|
| Panel History: |
|
|
Summary on Grant Application Form |
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.
|
|
Key Findings |
|
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
|
|
Potential use in non-academic contexts |
|
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
|
|
Impacts |
|
| Description |
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk |
| Summary |
|
| Date Materialised |
|
|
|
|
Sectors submitted by the Researcher |
|
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
|
| Project URL: |
|
| Further Information: |
|
| Organisation Website: |
http://www.leeds.ac.uk |