Stream: Miscellaneous

Topic: Readings on equality relation


view this post on Zulip Evgeniy Shishkin (Jul 22 2020 at 11:38):

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.

view this post on Zulip jco (Jul 22 2020 at 11:40):

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

view this post on Zulip Evgeniy Shishkin (Jul 22 2020 at 11:49):

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 )

view this post on Zulip Alexander Gryzlov (Jul 22 2020 at 12:22):

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"

view this post on Zulip Alexander Gryzlov (Jul 22 2020 at 12:24):

it's a bit old so it ends on OTT and doesn't mention HoTT

view this post on Zulip Evgeniy Shishkin (Jul 22 2020 at 12:36):

Thanks! We leave the HoTT equality for breakfast.

view this post on Zulip Bas Spitters (Jul 22 2020 at 19:09):

We tried to make the HoTT book accessible, and I believe with some success...

view this post on Zulip Karl Palmskog (Jul 22 2020 at 19:25):

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.

view this post on Zulip Bas Spitters (Jul 22 2020 at 19:28):

Perhaps mostly accessible to mathematicians, but I'm told quite a few people have read it by them selves.

view this post on Zulip Karl Palmskog (Jul 22 2020 at 19:29):

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.

view this post on Zulip Karl Palmskog (Jul 22 2020 at 19:39):

I guess I will have to wait for the "Practical HoTT" or "HoTT for computer scientists" book

view this post on Zulip Paolo Giarrusso (Jul 23 2020 at 13:07):

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.

view this post on Zulip Karl Palmskog (Jul 23 2020 at 13:11):

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.

view this post on Zulip Paolo Giarrusso (Jul 23 2020 at 13:36):

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).

view this post on Zulip jco (Jul 23 2020 at 14:53):

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

view this post on Zulip Hugo Herbelin (Jul 23 2020 at 14:56):

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:

Here are a few properties of an equality:

The structure of equality proofs gives rise to:

Indeed, there are also interactions between the equality of a theory as a proposition and the (meta)equality of the metatheory:

In another direction, we can make a difference between:

view this post on Zulip Karl Palmskog (Jul 23 2020 at 15:43):

@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

view this post on Zulip Hugo Herbelin (Jul 23 2020 at 17:22):

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.

view this post on Zulip Karl Palmskog (Jul 23 2020 at 18:38):

https://github.com/coq/coq/wiki/Equality -- initial version, I might polish a bit more at some later point

view this post on Zulip Karl Palmskog (Jul 23 2020 at 18:38):

I would probably add setoids on the one hand and bisimilarity on infinite coinductive types on the other hand

view this post on Zulip Karl Palmskog (Jul 23 2020 at 18:47):

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.

view this post on Zulip Paolo Giarrusso (Jul 24 2020 at 22:49):

I’m used to definitional and judgmental being equivalent (in ITT); where I‘ve seen a distinction, definitional equality stayed decidable


Last updated: Aug 19 2022 at 20:03 UTC