Comment by js8
13 hours ago
I tried to read HoTT. First chapter on type theory is great and pretty easy to follow. The second chapter, I got completely lost. I don't remember why, maybe they fixed it since.
But I find univalence axiom intriguing. I am interested in different approach to types, using triage calculus, which is more "materialist" than "structuralist" - type is given by the structure of the (quoted) term in normal form (unlike lambda calculus, triage calculus makes quoting easy). And I feel like univalence is related to quoting, something like if the two quoted terms are equal under "standard self-interpreter", then they are equal.
I would highly recommend "PROGRAM = PROOF" by Samuel Mimram.
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...
This is probably a reasonable example of a case where an AI can really help out as an endlessly patient assistant to answer your personal questions in a conversational format.
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.
Yes, maybe.. I read it like a decade ago though, the AI didn't exist then. Although my current interest in triage and lambda calculus is also fueled by AI.
> I am interested in different approach to types, using triage calculus, which is more "materialist" than "structuralist" - type is given by the structure of the (quoted) term in normal form (unlike lambda calculus, triage calculus makes quoting easy).
Interesting, dropping this link here for others: https://treecalcul.us/
Yes. In type theory, the term carrying a type is a metalogical notion. In triage calculus, you can define a typechecking program that operates on a quoted term and normalizes only if the term typechecks.
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.
HoTT distinguishes equality from equivalence.
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.
Yeah, but a similar thing works with programs (terms in normal forms in triage calculus). There is equality of terms and equivalence with respect to beta reduction.
(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.