Zulip Chat Archive

Stream: new members

Topic: equiv

abaaba (Mar 03 2022 at 16:16):

Why does equiv means equivalence relationship? It only encapsulates a bijective function and its inverse.


Riccardo Brasca (Mar 03 2022 at 16:19):

As written just below the definition, α ≃ β is the type of functions from α → β with a two-sided inverse, so equiv doesn't mean "equivalence relation" here. α ≃ β is the type (read set if you prefer) of bijective functions α → β.

abaaba (Mar 03 2022 at 16:22):

α ≃ β is the type (read set if you prefer) of bijective functions α → β.

I see. But how is that related with word "equivalence"?

Riccardo Brasca (Mar 03 2022 at 16:24):

I think the name comes from equivalent set, i.e. sets with same cardinality, i.e. α and β are equivalent if there is a bijection α → β. Then of course being equivalent is an equivalence relation.

Chris B (Mar 03 2022 at 16:40):

At the top, the docs do say it's an equivalence between types ... used to express that Types/Sorts are equivalent, not that this is "the notion of an equivalence relation". You might be more satisfied with https://leanprover-community.github.io/mathlib_docs/init/logic.html#equivalence.

abaaba (Mar 03 2022 at 16:51):

Oh I see, but honestly what a confusing naming .... equivalent set means sets with same cardinality ....
And still, why does the page says "we use this (and not equality!) to express that various Types or Sorts are equivalent." Does the "equivalent" here also means the type have same cardinality (or in case of infinite types, have a bijection relation between them)?

Riccardo Brasca (Mar 03 2022 at 16:56):

Equality of type is an evil concept, you should almost always avoid it. Yes, "equivalent" means "same cardinality". This is common mathematical terminology.

Sebastian Reichelt (Mar 03 2022 at 18:13):

Note that it has refl, symm, and trans that have the same form as an equivalence relation, except that Prop is replaced with a more general Sort.

Reid Barton (Mar 03 2022 at 18:14):

Honestly I think "equivalence" is a weird word to use for this from the standpoint of ordinary math--maybe it comes from intensional type theory/homotopy type theory?

Reid Barton (Mar 03 2022 at 18:14):

I would just say isomorphism (or bijection)

Reid Barton (Mar 03 2022 at 18:22):

Maybe it depends on your native language

Yakov Pechersky (Mar 03 2022 at 18:41):

What is additionally confusing is that we have docs#has_equiv which is used for notation for equivalence relations (via setoid instances)

Junyan Xu (Mar 03 2022 at 20:40):

An equiv is an explicit bijection / 1-1 correspondence, usually a canonical one, it's not a Prop so not just "having same cardinality"; docs#cardinal.is_equivalent is defined to be the Prop nonempty (α ≃ β). It can be used to state that two structures are cryptomorphic, i.e. are mathematically equivalent concepts, and carries the functions to go between them.

Kevin Buzzard (Mar 03 2022 at 23:08):

I was also very confused by the usage of the word "equivalence" and the abbreviation equiv for this concept, when I started learning Lean. It's one of those things like "lift" which you kind of feel you're stuck with; maybe when mathematicians are writing their own theorem provers they can use language we find more appropriate.

Reid Barton (Mar 04 2022 at 00:05):

or "type"

Kevin Buzzard (Mar 04 2022 at 00:17):

It's just another word for "set"

Mario Carneiro (Mar 04 2022 at 00:19):

set, kind, sort, collection, group, type, conglomerate

Mario Carneiro (Mar 04 2022 at 00:20):

we're really hard on synonyms for "bunch of stuff"

Mario Carneiro (Mar 04 2022 at 00:22):

to the point that it becomes difficult to have plain english discussions about bunches of stuff because you have to avoid all the synonyms that have been given a technical meaning

Jakub Kądziołka (Mar 04 2022 at 00:34):

I propose murder (as in of crows, not of mathematicians)

Yaël Dillies (Mar 04 2022 at 00:38):

You mean you can't have a normal conversation because mathematicians lack an inner product?

Jakub Kądziołka (Mar 04 2022 at 00:42):

wah, I don't get it

Yaël Dillies (Mar 04 2022 at 01:13):


Arthur Paulino (Mar 04 2022 at 02:42):

This is probably because of my CS background, but the idea of "set" doesn't work well as a replacement for "type" in my mind. Things of the same "type" are necessarily intimately related by their nature, whereas things of the same "set" may not, depending on how the set was built.

This is probably dependent on mother tongue, but from those words that Mario listed, "type", "sort" and "kind" are the true synonyms for me. And the other words would form another cluster of synonyms

Arthur Paulino (Mar 04 2022 at 02:44):

And there goes another word: "cluster" :upside_down:

Last updated: Dec 20 2023 at 11:08 UTC