Lean Formalisation of Two-Level Type Theory
Files in the
|fibrant.lean||implementation of the two-level type theory|
|finite.lean||facts about finite sets and categories with a finite set of objects|
|limit.lean||definition of limits and construction of limits in category of pretypes|
|inverse.lean||definition of inverse categories (Section 4.2)|
|pullbacks.lean||definition of a pullback, constructed explicitly and using the limit of a diagram along with a proof these definitions are equivalent. Proof of that fibrations are closed under pullbacks.|
|matching.lean||definition of the matching object (Section 4.3)|
|matching_facts.lean||facts about the matching object from the category C with one object removed|
|fibrantlimits_aux.lean||auxiliary lemmas for the proof of the fibrant limits theorem including equivalences forming the core of the proof|
|fibrantlimits.lean||a proof of the fibrant limit theorem (Section 4.3, Theorem 4.8.)|
|simplicial.lean||initial definition of semi-simplicial types (work in progress)|
|facts.lean||some auxiliary lemmas which we could not find in the standard library|
|types/*||some examples of reasoning in the inner (fibrant) theory. Mainly, ported from the Lean 2 HoTT library.|
Requires Lean 2 (version 0.2.0) to compile.
Lean 2 installation instructions in Ubuntu : https://github.com/leanprover/lean2/blob/master/doc/make/ubuntu-12.04-detailed.md
After installing Lean 2, in the terminal, go to the directory containing the development and use
make to compile the project, or run go to the
2ltt folder and run
Use your favorite editor to navigate the source code (see some hints about emacs lean-mode blow).
Docker image. The image is based on Ubuntu and contains Lean 2, our development and Emacs with
lean-mode, allowing to navigate through the development and compile it.
Steps to build a Docker image:
- In the terminal, go to the directory containing the development and run
- After building step is complete (this might take some time), run
make run-imageto connect your current terminal session to the container.
- In the container, type
emacs /root/2ltt/fibrantlimits.leanto start editing
fibrantlimits.leanwith the lean-mode in Emacs.
Interacting with the Lean development in the Docker image
As we have said before, the docker image comes with Emacs and lean-mode. The lean-mode provides syntax highlighting and allows to interactively develop proofs. Use C-c C-g to show goal in tactic proof, C-c C-p to print information about identifier, C-c C-t to show type, and C-c C-l to comple a lean file.
Alternatively, one can use the command line to compile the project or individual files:
- After executing
make run-image, change directory (in the Ubuntu's command line) to our Lean development
make cleanto clean previously compiled files
makeagain to rebuild the project.
- Individual files can be compiled using
The image comes with the preinstalled
nano editor that can be used to view/edit the source files (but without syntax highlighting). Other editors can be installed, if required, using the
apt-get command. For example,
apt-get install vim.