Homotopy type theory in Lean 3
This repository contains a work-in-progress port of the Lean 2 HoTT library to Lean 3.
- No modifications to the Lean kernel are made. Since the Lean 3 kernel is inconsistent with univalence, we "disable" singleton elimination. Singleton elimination is the property that some
Prop-valued inductive types (where terms can only be constructed in one way) can eliminate to
Type. The main example is that the equality type
eqwhich is defined to be in
Propcan eliminate to
Type, which is inconsistent with univalence. Whenever a definition/theorem with the
[hott]attribute uses singleton elimination, we print an error. Currently we need to add this attribute to all definitions, but in future we expect to say once at the top of a file that all definitions/theorems in that file have the
[hott]attribute. Without singleton elimination the system is conjectured to be consistent (if it isn't, we can easily extend the check).
- We add univalence as an axiom.
- We add HITs using Dan Licata's trick. Declarations with the
[hott]attribute are checked to not use the internal inconsistent induction principle for HITs.
- We try to write domain-specific automation using the powerful metaprogramming language of Lean 3
- All declarations in Lean 3
initare available. This is necessary to get the basic tactics. This also means that some "unsafe" tactics are available which use the
- don't use
casessometimes uses singleton elimination. In this case, try replacing it with
dsimpis useful for definitional simplifying. It will rewrite all equalities marked with
[hsimp]. Furthermore you can use
dsimp [foo]to unfold/rewrite with
dsimp only [foo]if you don't want to do anything else). For non-definitional simplifying, use
- don't use
- Feel free to help porting with files.
- If you want you can open an issue to ask which files are currently being ported
- For your convenience you can look here for files where some common changes are made with a simple regex-replace.
- If you port a file from Spectral, make sure it hasn't been modified since september 2017.
- Modify the file to fix all errors in Lean 3. Common changes are listed here
- Make a pull request.
- Feel free to write any domain specific automation you want. Incomplete wishlist:
- A better algorithm to prove truncatedness and connectedness
- A simple equivalence-maker (for example to prove that structures are sigma types)
- A induct-on-everything tactic (or maybe just induct-on-all-paths and destruct-all-pointed-objects)
- Maybe some tactic other than
dsimpto do simplification on the goal which has the functionality of
esimpin Lean 2.