equiv

Stream: new members

[abaaba]

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

https://leanprover-community.github.io/mathlib_docs/data/equiv/basic.html#equiv

[Riccardo Brasca]

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]

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

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

[Riccardo Brasca]

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]

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]

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]

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]

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]

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]

I would just say isomorphism (or bijection)

[Reid Barton]

Maybe it depends on your native language

[Yakov Pechersky]

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

[Junyan Xu]

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]

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]

or "type"

[Kevin Buzzard]

It's just another word for "set"

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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]

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

[Yaël Dillies]

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

[Jakub Kądziołka]

wah, I don't get it

[Yaël Dillies]

(orthonormality)

[Arthur Paulino]

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]

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