0
$\begingroup$

In appendix A1 of the homotopy type theory book by the Univalent Foundations Project, the authors give a formal presentation of Martin-Löf type theory in lambda calculus. However, they did not give any formulation of univalence or any higher inductive types in appendix A1. The circle type does appear later in appendix A3, as well as univalence, but both were formulated in natural deduction rather than in lambda calculus.

How would one go about defining univalence and higher inductive types (say the circle type) in the lambda calculus model of Martin-Löf type theory?

Improve this question
$\endgroup$
3
  • $\begingroup$ What is the “$\lambda$-calculus model of type theory“? Anyhow, at the time of writing the HoTT book we did not know how to give a formal presentation of higher inductive types. Univalence was just the postulate that a certain type is inhabited – for a more structurally type theoretic account something like cubical type theory had to be invented first. And that did not exist either at the time of writing. $\endgroup$
    – Andrej Bauer
    Commented Oct 28, 2022 at 6:22
  • $\begingroup$ The first sentence of appendix A1 of the HoTT book states that "The objects and types of our type theory may be written as terms using the following syntax, which is an extension of λ-calculus with..." As a result, I am calling whatever is being formally defined in appendix A1 the λ-calculus model. $\endgroup$
    – Madeleine Birchfield
    Commented Oct 28, 2022 at 8:39
  • $\begingroup$ I think I am getting thrown by the word “model”, which is a semantic notion. I would say “λ-calculus formalism” or something like that. $\endgroup$
    – Andrej Bauer
    Commented Oct 28, 2022 at 10:17

0

Reset to default

You must log in to answer this question.

Browse other questions tagged .