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