I've read a few slides on the topic citing the following quotation from an email, which, according to these slides, defines the biggest advantage of homotopy lambda calculus over other caculi of induction:
[. . . ] My homotopy lambda calculus is an attempt to
create a system which is very good at dealing with
equivalences. In particular it is supposed to have the
property that given any type expression F(T) depending on
a term subexpression t of type T and an equivalence t → t'
(a term of the type Eq(T; t, t')) there is a mechanical way to
create a new expression F' now depending on t' and an
equivalence between F(T) and F' (T') (note that to get F'
one can not just substitute t' for t in F – the resulting
expression will most likely be syntactically incorrect).
- Email from Vladimir Voevodsky to Daniel R. Grayson, Sept 2006
[1]
Can you give a real example of this "mechanical way"? The best examples would be if it is already implemented in any programming or proving language (since this is where type theory should be applied to).
Thanks you so much for you insight.
UPDATE 1: Sorry for not including references immediately. This is my first post so I don't know the rule here:
[1] Ahrens, Benedikt, and Paige Randall North. "Univalent foundations and the equivalence principle." Reflections on the Foundations of Mathematics. Springer, Cham, 2019. 137-150. (https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.721.59&rep=rep1&type=pdf)
(The original email is archived: https://inbox.vuxu.org/hott/[email protected]/t/, the link may be obsolete in the future)
For future reference, it would be easier to answer the question if you provided a link to the slides in question. However, I can try to answer it anyway.
The "homotopy lambda calculus" to which Voevodsky referred in this email 15 years ago never really came to fruition by that name. Instead he discovered Martin-Lof type theory and formulated his Univalence Axiom for it, and this led to the subject now known as Homotopy Type Theory / Univalent Foundations (HoTT/UF). The desideratum that Voevodsky mentioned in the email you cite is essentially achieved by the univalence axiom: given $e : \mathrm{Eq}(F;t,t')$, we can "apply" $F$ to this equality to get $\mathrm{ap}_F(e) : \mathrm{Eq}(U,F(T), F(t'))$, where $U$ is the universe of types, and the univalence axiom says that $\mathrm{Eq}(U)$ consists of equivalences.
The original version of HoTT/UF, as formulated for instance in the homotopy type theory book, was not computational, so that the actual equivalence $\mathrm{ap}_F(e)$ could not be computed "mechanically" by a computer. This has since been remedied by the development of Cubical Type Theories, which are implemented in several more or less experimental proof assistants but notably Cubical Agda. The latter cited paper on Cubical Agda has several examples of how this property is used.