Alexander Kuklev (akuklev) wrote,
Alexander Kuklev

Untyped model of HoTT

One can model terms of Σ-types, Π-types, inductive type families and Tarski universes (modelled by type families having type formers as introduction rules) by untyped lambda terms using Parigot encoding[1,2] that allows for direct translation of type-theoretic introduction and elimination rules that guarantees that type-theoretic definitional equalities translate to equivalence of lambda terms, i.e. judgemental equality yields substitutional equality of lambda terms.

The only problem with model of MLTT on (equivalence classes) of untyped lambda terms are the Id-types, I'm not aware of any encoding for them that makes J rule compute, but now I have great hopes for something like extended cubical lambda calculus that would be able to serve as untyped computational model for HoTT (and intensional MLTT without K rule in particular).

[1] Peng Fu, “Lambda encodings in type theory”,
[2] Peng Fu, Aaron Stump, “Self Types for Dependently Typed Lambda Encodings”,

  • (no subject)

    Встретил фотографию толпы футбольных фанатов, и она меня скорее напугала, у меня уж точно нет желания быть там среди них. Но внезапно я понял, что…

  • Прогресс

    Десять дней назад, вторая ступень SpaceX'овского корабля Starship своим ходом слетала своим ходом на десять километров вверх, и усмепшно приземлилась…

  • О водосбережении

    Как известно, питьевая вода во многих странах дефицитный ресурс. И даже в дождливой Германии летом иногда случаются засухи, в результате которых она…

  • Post a new comment


    default userpic

    Your reply will be screened

    Your IP address will be recorded 

    When you submit the form an invisible reCAPTCHA check will be performed.
    You must follow the Privacy Policy and Google Terms of use.