Homotopy Finiteness

This repository is a formalisation of Rijke's proof that the number of groups of finite order is finite [3] in Jonas Hoefer's prototype.

The goal of this implementation is to better understand the computations done and, if possible, derive and formalise a new proof, "better" (for some definition of better) proof.

An HTML rendering of the formalization is available at this URL.

Setup

Everything needed to execute this project is bundled into this repository. Beware that the cloning must happen to download submodules. One way of doing it is as follows:

• in SSH:

git clone --recursive-submodules git@github.com:jrosain/Homotopy-Finiteness.git

• in HTTPs:

git clone --recursive-submodules https://github.com/jrosain/Homotopy-Finiteness.git

If you have already cloned the repository, no worries. Use the following command:

git submodule init && git submodule update

Once cloned, cd poset-type-theory and follow the installation instructions here.
Now, you should be able to run the command postt repl. Then, you should be able to load the main proof of this work:

:load -s src/Playground.ctt

Afterwards, you can unfold to compute the number of groups of order, say, one up to isomorphism:

:unfold number-of-Group-of-Order-one

Emacs modes

A small emacs mode has been developed so that org-mode can be used to formalize things. It can be found in the folder emacs-mode/ and loaded with M-x load-file RET emacs-mode/ob-ctt.el. It then suffices to press C-c C-c (in a code block) to evaluate a file. It also contains a copy of the minimal major mode that can be found here, with some additional tweaks to beautify the often-used symbols.

Organisation of this repository

The goal of this repository is twofold:

• develop a library of standard results following [1, 2] ;
• formalize the homotopy finiteness proof of [3].

As such, it is organized as follows: the src/Lib folder contains the standard results, that should be merged in the standard library of the language at some point, and the other files of the src/ folder contain the formalization of [3].

Some name and proofs of src/Lib have been adapted from [4].

References

1. Introduction to Homotopy Type Theory, Egbert Rijke (2022), https://arxiv.org/abs/2212.11082
2. The HoTT Book, The Univalent Foundation Program (2013), https://homotopytypetheory.org/book/
3. Daily applications of the univalence axiom, Egbert Rijke (2022), Logic and Interactions in the Centre International de Rencontres Mathématiques (Marseille, France).
   slides, talk
4. Agda Unimath Library, https://unimath.github.io/agda-unimath/HOME.html