Higher Observational Type Theory

Introduction

Recent advancements have enabled proof assistants to formally verify world-class mathematics: the liquid tensor experiment, the four colour theorem, and the odd order theorem were formalised. Computer-checked arguments are important for mathematicians who want to be certain their reasoning is sound, and for computer scientists to prevent bugs in safety-critical software.

Examples of Formal Verification

Examples include:

• Formally verified parts of Google's Chrome web browser
• Verified implementations of the C and ML programming languages

Type Theory Foundation

At the core of these formalisations lies type theory, upon which proof assistants are built. Type theory is both a functional programming language and a foundation of mathematics.

Emergence of Higher Dimensional Spaces

Recently, models of type theory built on higher-dimensional spaces emerged, where:

• Elements of a type are points in the space
• Elements of an equality type are paths in the space

Based on these, type theory was extended to homotopy type theory (HoTT), featuring the principle that isomorphic types are equal. This moves formalisation close to actual mathematical practice where isomorphic structures are treated as the same.

Challenges in Adoption

While HoTT is successful among academics, it hasn't been widely adopted. This is because type theories implementing HoTT rely on an explicit syntax for higher-dimensional geometry, which is conceptually difficult and hard to use in practice. This creates a substantial barrier for formalisation, which is treated as a low-level, bureaucratic process.

Project Goals

Our project will develop a radically new type theory where homotopical content is emergent, rather than built-in. The idea is to define the equality type via computation.

Benefits of the New Approach

This approach makes HoTT explainable and conceptually simple. It also improves pragmatic aspects:

• With more computation, proofs become less tedious.

Our theory will contribute to a new era in the formalisation of mathematics and verification of software, where developing proofs in abstract, reusable ways becomes standard, accelerating progress in both areas.