It covers everything from pure lambda calculus through dependent type theory up to homotopy type theory. In comparison to the HoTT book, the book "PROGRAM = PROOF" is oriented less towards mathematicians more towards programmers. It contains also a short introduction to OCaml and Agda.
The book can downloaded from the authors web page:
https://www.lix.polytechnique.fr/Labo/Samuel.Mimram/teaching...
https://www.lix.polytechnique.fr/Labo/Samuel.Mimram/publicat...
It is possible it may get something wrong but as long as you keep beating on the wrongness you should eventually be able to work out what it is, and in its own way that would become possibly the best learning exercise there is. And of course, with the math proofs coming through from AIs lately, I wouldn't guarantee you'll see that much wrong stuff. I expect it would be at a low enough rate to keep you learning... after all, anyone who has had serious math education knows the human teachers aren't always completely correct either and there is the occasional impromptu exercise of everyone staring at the board and trying to figure out what went wrong with the demonstration.
Interesting, dropping this link here for others: https://treecalcul.us/
This means in triage calculus (unlike in lambda calculus, which lacks means to quote programs) you can include expected input data types in your programs.
You can also construct any type theory syntactically by putting together a set of terms in triage calculus which only normalize when composed with correct types.
In triage calculus, you can then study types and propositions as any other programs - using self-interpretation. But I believe, as I detail below, a univalence principle is needed, to postulate the equivalence of metalogical triage calculus and its representation within triage calculus.
Univalence says that equality is equivalent to equivalence, ie, formalizing the notion of when we can use equivalence rather than equality as a step in a proof. In practice, we often only care about proofs “up to equivalence”.
A way to think about this:
- equality is an identity map
- equivalence is an isomorphism
For example, 2 in Z and 2 in R do not have an identity map between them — but do have an isomorphism.
I think the key insight of univalence is not collapsing equivalence into equality — but allowing it to remain a second truth relation.
We don’t want 2 in Z to be equal to 2 in R (because we collapse type distinction), but we do want them to be equivalent — so we can do equivalent reasoning about arithmetic in R to reach conclusions about Z.
(I used equal to mean the latter, this is colloquial, so I should watch my language.)
And what I am saying in my version of univalence is not that these two are the same, but rather, we can simulate beta-reduction equivalence using self-interpretation.
My version of the axiom states, that two terms x, y are beta-equivalent iff the term interpret(quote(x)) is beta-equivalent to term interpret(quote(y)).
(Note that quote() is identity function in triage calculus, I only write it for clarity.)
So my axiom postulates that the metalogical notion of equivalence is equivalent to the one we can study using whatever interpret() - a self-interpreter - is.
Whether my axiom is related to univalence in HoTT, I am not sure. But it feels similar.