Higher Observational Type Theory

Recent advancements have enabled proof asistants 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 are formally verified parts of Google's Chrome web browser and verified implementations of the C and ML programming languages.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.

Recently, models of type theory built on higher dimensional spaces emerged, where elements of a type are points in the space, and elements of an equality type are paths in the space.

Based one 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 being treated as the same.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, bureaucractic process.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. This 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 formalisation of mathematics and verification of software, where developing proofs in abstract, reusable ways becomes standard, accelerating progress in both areas.