This repository contains a work-in-progress port of the Lean 2 HoTT library to Lean 3.
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 eq
which is defined to be in Prop
can 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).[hott]
attribute are checked to not use the internal inconsistent induction principle for HITs.init
are available. This is necessary to get the basic tactics. This also means that some "unsafe" tactics are available which use the Prop
-valued equality.
rewrite
, use rwr
insteadcases
sometimes uses singleton elimination. In this case, try replacing it with induction
.dsimp
is useful for definitional simplifying. It will rewrite all equalities marked with [hsimp]
. Furthermore you can use dsimp [foo]
to unfold/rewrite with foo
(or dsimp only [foo]
if you don't want to do anything else). For non-definitional simplifying, use hsimp
.dsimp
to do simplification on the goal which has the functionality of esimp
in Lean 2.