theckl / chott4 Goto Github PK

This repository hosts the Lean 4 development of a model of Cubical Type Theory in Homotopy Type Theory, with a proof of Function Extensionality, Univalence and the construction of Higher Inductive Types. We follow the construction of a set-theoretic model of Cubical Type Theory in the paper of Cohen, Coquand, Huber and Mörtberg (and hope that higher equalities are not needed). An immediate consequence of such a model is the "canonicity" of Cubical Type Theory, with its consequences for decidability of judgmental relations, simply because those hold for Homotopy Type Theory not assuming Univalence and HITs as axioms.

The development must avoid some features of Lean 4 that are not consistent with Homotopy Type Theory. The cleanest but maximal solution is to avoid all types of Sort 0. In the HOTT3 library based on Lean 3 only singleton elimination is disabled. Both strategies can be implemented by attributes, but the latter may be simpler and more efficient. In any case, at the moment it is beyond my abilities to program attributes.

We also need to redefine equality between two objects of a type: It is a type of arbitrary universe level, not just a Sort 0. We achieve this by placing all the development inside a namespace hott, as in the HOTT3 library. Overall, we plan to "port" most of the HoTT specific definitions from this library, also following its folder structure.