alt Hacker NewsI 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.
Replies
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.
> 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/
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.
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...