A followup to my previous email in another discussion (copied below).

I said in that email that the kernel of Lean 3 is inconsistent with
univalence. While this is true, we are currently developing a HoTT library
for Lean 3 here:
https://github.com/gebner/hott3
The logic in this library is consistent in the following sense described
below.

In Lean you can define inductive types and inductive propositions. Most
inductive propositions can only eliminate to Prop (having them eliminate to
Type would be inconsistent with proof irrelevance). There is a rule called
singleton elimination, which allows certain propositions which are
"subsingletons" to eliminate to all types (I believe that an inductive type
is a subsingleton if it has at most one constructor, and all arguments of
that constructor are Prop-valued, but don't quote me on that).

In the Lean 3 HoTT library Gabriel Ebner has written a program that checks
whenever you proof a theorem/definition in the HoTT library that singleton
elimination is not used. If it is used, then it raises an error (even
though the Lean kernel did accept the proof).

We're quite certain that removing singleton elimination makes the kernel
consistent with univalence. In fact, I believe that even when assuming
`false` (which is the empty type living in Prop) we cannot construct any
data in a type from it. This allows us to write metaprograms, like tactics
and automation in Lean using Prop, while not using Prop in the HoTT-library.

I think Lean 3 is an interesting proof assistant to work on HoTT-specific
automation, since Lean has a very strong metaprogramming language to write
tactics in the Lean language itself. It is probably not the long-term
"best" proof assistant, since its underlying type theory is not cubical
(its underlying type theory is basically the type theory of the HoTT book).
Work is in progress to port the formalizations from Lean 2 to Lean 3.

For more information see the readme of the linked Github repository. Any
comments are welcome.

Best,
Floris



On 17 December 2017 at 23:43, Floris van Doorn <fpvd...@gmail.com> wrote:

> Just to clear some things up in this conversation:
>
> - The Lean kernel is consistent with any form of propositional
> extensionality, as far as I know.
> - The kernel for the current version of Lean, Lean 3, is not designed for
> HoTT and inconsistent with univalence. However, it does *not* ignore any
> transport of an equality. The bottom universe in Lean is the universe of
> propositions, Prop (not to be confused with hProp). What does hold is that
> there is definitional proof irrelevance for proofs of a proposition, i.e.
> if P : Prop and p, q : P then p is definitionally equal to q. This means
> that if we have a proof p : A = A for some type A, then transporting along
> p is the identity function (because p = refl, definitionally). However, if
> p : A = B, then transporting along p is not the identity function (which
> would be type incorrect to state).
> - Lean has an evaluator in a virtual machine, which is used to evaluate
> programs and tactics efficiently outside the kernel. This evaluator is not
> trusted, and cannot be used when writing any proof in Lean. This evaluator
> removes all type information and propositions for efficiency, and can
> evaluate expressions to the wrong answer when axioms are added to the type
> theory (even if the axioms are consistent). For example, if we add the
> following lines to Ben's example
> ```
> constant H : HProp_ext
> #eval Sig.fst (x H)
> ```
> we see that the evaluator incorrectly evaluates this expression to tt
> (true). Needless to say, the evaluator was not designed for this, but
> instead to evaluate tactics like the following quickly.
> ```
> if n < 1000000 then apply tactic1 else apply tactic2
> ```
>
> I hope this clears up any confusion.
>
> Best,
> Floris
>
>