lean-type-theory

Computation is the difference. In Lean, applying the universal property of the quotient (`Quotient.lift f Hf`) to an element that is of the form `Quotient.mk a` reduces to `f a`. This rule is fine in itself, but the Lean developers were not sufficiently careful and allowed it to apply for quotients of propositions, where it interferes with the computation rules for proof irrelevance and ends up breaking subject reduction (SR is deeply linked to computation when you have dependent types!) [0]. It is not really a problem in practice though, since there is no point in quotienting a proposition. [0] see the end of section 3.1 in https://github.com/digama0/lean-type-theory/releases/downloa...

Yup, Lean's quotient induction breaks subject reduction, which is an important type-theoretic principle. It means you can write a Lean development where t has type A, and t reduces (i.e. computes, as part of the Lean kernel) to u, but u doesn't have type A, and may not even type check. (See https://github.com/digama0/lean-type-theory/releases/downloa... Sec. 3.1 for a detailed discussion of this issue.) This is obviously quite bad, and it goes far beyond the usual drawback of adding axioms to a theory, including the quotient axiom. (Namely, the loss of canonicity.)

Mario Carneiro’s MS Thesis has a good overview of the type theory and how it compares to Coq: https://github.com/digama0/lean-type-theory/releases/downloa...

I wrote two reference type checkers for Lean and learned a lot about both the Lean kernel and the implementation of DTT; it's not an easy exercise, but I would recommend it. The ones I wrote are in a language that's not the easiest to read (though I did end up getting the performance to justify the language choice), but if any related questions come up feel free to contact me and I'll do my best to give a coherent answer: https://github.com/ammkrn/nanoda_lib This paper on Lean's type theory dovetails nicely with any of the kernel implementations: https://github.com/digama0/lean-type-theory/releases/tag/v1.... Also this article is really neat, thanks OP. These kinds of visual representations and other alternative mediums you can use to document stuff are (imo) a really important and under-explored area.