Bonak is an active hobby-research project around formalizing simplicial and cubical sets in Rocq as a particular case of iterated parametricity translation. The project started when Hugo met Ram in late 2019, and they continue to meet online weekly to continue this line of research.
The name bonak comes from an imaginary monster in Daisy Johnson's novel Everything Under, which was shortlisted for the Booker Prize in 2018. It happens to be an exciting read, and Ram had read the book at around the time this project started.
Some features of this project:
- We do not make use of HoTT, or any fancy libraries for that matter. Bonak is written is vanilla Rocq, making use of the core standard library. In particular, we make heavy use of SProp for definitional proof irrelevance.
- Bonak has led to many bugs being filed and fixed in core Rocq. It pushes the boundaries of proof assistant technology, and can serve as a benchmark against which to improve core Rocq features. Rocq 9.0 is required to build the current version.
- As the main contribution of Bonak is the Rocq code, we have placed high emphasis on code cleanliness and readability. As a result, it's quite pleasant to step through the code, and have a succinct goal at all times.
- Bonak is tiny! In ~900 lines of Rocq code, we have managed to prove something remarkable. We did have a lot of false starts, and tried various approaches, before settling on what we have today.
Axioms:
functional_extensionality_dep
: forall (A : Type) (B : A -> Type) (f g : forall x : A, B x),
(forall x : A, f x = g x) -> f = gOur approach is generic over the arity of the parametricity translation: we use functional extensionality for this, but it can, in principle, be done without this axiom for any fixed finite arity.
The first paper describing our initial work can be found at arXiv:2401.00512 (pre-print) or 10.1017/S096012952500009X (published version), and the corresponding code can be found under the tag hr25.
master and other branches contain work-in-progress for future publications.