Hi! Do you have suggestions on what to read about an equality relation in a context of constructive logic: what it is, what kinds of equality relation are discovered so far, etc.
Evgeniy Shishkin said:
Hi! Do you have suggestions on what to read about an equality relation in a context of constructive logic: what it is, what kinds of equality relation are discovered so far, etc.
I was thinking about asking this a couple days ago, glad someone else did. Reading up on this stuff there's a lot of discussion of Hott, JMeq (axiom K) etc...equality is big business
Yeah, Ideally, I would like to read some not at all shallow overview of an equality relation in different subfields of logic or math in general, with links to more a advanced reading. Thanks to the community, I am sure those guys - titans of thought - have a lot to suggest on this )
I guess one could start from something like
http://kodu.ut.ee/%7Evarmo/tday-andu/chapman-slides.pdf Chapman, "A biased history of equality in type theory"
it's a bit old so it ends on OTT and doesn't mention HoTT
Thanks! We leave the HoTT equality for breakfast.
We tried to make the HoTT book accessible, and I believe with some success...
I remember skimming the HoTT book when it came out, but to me it was a mystery who it was for (i.e., accessible to whom, and for what purpose). So maybe one answer is: it has a modern discussion of equality in type theory.
Perhaps mostly accessible to mathematicians, but I'm told quite a few people have read it by them selves.
For example, I think the page "About this book" is not really a description of what the book is or what it tries to accomplish.
I guess I will have to wait for the "Practical HoTT" or "HoTT for computer scientists" book
I will agree the HoTT book is much more accessible than the typical book for graduate mathematicians (even tho the topic is not easy). I will confess I have a modicum of intuition about topology (at a level between pop-sci/1st year math BSc), which is probably more than is common in CS.
is there really any place for topology at all in a BS/MS level CS curriculum outside trivial overlaps with linear algebra, graph theory, etc.? My view is that there basically isn't (and this is the case in nearly all US/European universities I'm familiar with), so I think the HoTT book is not particularly CS-background-welcoming.
I'm sure you are right and I'm suffering from a knowledge bias. There's nothing I dislike more than mathematicians who say "X is easy" when all they know is "I understand X intuitively". But at the risk of committing that same sin: IIRC the first chapters require nothing more than "rubber-sheet topology".
If there is a gap, I think the missing material can be made accessible even to (good) high-school students, if you're willing to be informal (and probably silently use classical reals).
I feel like writing "hott for computer scientists" is a good way for some academic to get famous :)
but it's nice to hear that the topological knowledge necessary is not so intense
If ever useful, I may share my own recollection of what I understand about equality (this is a personal view and I'd actually be interested in feedback about it).
We can distinguish different strengths of equality:
x ⊢ t = u
implies ⊢ λx.t = λx.u
Here are a few properties of an equality:
The structure of equality proofs gives rise to:
trans p (trans q r)
is syntactically different from trans (trans p q) r
and we need to write an explicit proof term of the equality of trans p (trans q r) = trans (trans p q) r
, and recursively, and there are different provably equal but not syntactically equal proofs of this latter statement. So, what really matters is whether the equality up to equality (and recursively in further nestings of equality) is strict or not, and if strict, whether there is a decidable subset of it that could be managed automatically at the meta-level in a proof assistant.Indeed, there are also interactions between the equality of a theory as a proposition and the (meta)equality of the metatheory:
judgemental equality, in the context of Martin-Löf's type theory, also called conversion in the context of Pure Type Systems, also called "equality on the nose" in the context of set theory, is used to quotient terms and types at the metalevel by a subset of strict equality.
It can be typed or not, decidable or not:
Its extent can also vary:
by contrast, equality as a connective is called propositional (and, of course, it includes the judgemental quotient).
In another direction, we can make a difference between:
vec (n+m) = vec (m+n)
) and it has the drawback that it has to be strict (i.e. it requires UIP); so, in my opinion, John Major equality is nowadays advantageously replaced by cubical equality, which is also an heterogeneous equality.@Hugo Herbelin can I post (reproduce) this on the Coq wiki? I think some of the non-Coq-using students in my group should read this
Sure. I realize that I forgot to mention also definitional equality (an oriented synonym of intensional as far as I can judge), ad hoc polymorphic equality (as in cubical or observational type theory), identity type, but I can add it afterwards. I may also try to compare with (e.g.) https://ncatlab.org/nlab/show/equality.
https://github.com/coq/coq/wiki/Equality -- initial version, I might polish a bit more at some later point
I would probably add setoids on the one hand and bisimilarity on infinite coinductive types on the other hand
Per Chlipala's CPDT, there will always eventually be another member of the equality zoo:
researchers are actively investigating new definitions of what it means for two terms to be equal.
I’m used to definitional and judgmental being equivalent (in ITT); where I‘ve seen a distinction, definitional equality stayed decidable
Last updated: Jun 10 2023 at 06:31 UTC