Wie erklärt man Typ versus Mengen?

[TentativeConvert]

Ich gebe hier mal kurz eine bereits länger zurückliegende Diskussion wieder (Email [2023-05-19]):

M:

… Ist das nicht vielleicht einer der entscheidenden Unterschiede zwischen Mengen und Typen[:] Mengen sind allein durch ihre Elemente definiert, Typen sind irgendwie komplizierter?

J:

Prinzipiell kann man Typen nur beschränkt miteinander vergleichen. Auf jeden Fall scheint das für mich nicht der entscheidende Unterschied zu sein. Ich würde behaupten, dass man Typen nicht einfach so miteinander vergleichen kann. In der Mathe kann man einfach etwas aufschreiben wie ℕ ∪ ℝ oder Hom(ℕ, ℝ) ∪ Hom(ℝ, ℝ) aber dafür muss man zuerst erklären wie man die Elemente beider Seiten vergleicht. …

A:

Verschiedene Typen können keine gemeinsamen Elemente enthalten. Die Elemente eines Typs werden durch die Konstruktoren des Typs definiert.

Mengen hängen immer von einem Typ ab und dürfen nur dessen Elemente enthalten. Die Elemente einer Menge werden durch ein Prädikat auf dem Typ definiert.

[TentativeConvert]

S, as summarized by M:
Think of a Type as a (homogeneous) set. Think of a set in Lean as subset. Note that we need to distinguish between a Type/set X, and X viewed as a subset of itself (univ X). In exactly the same way, we need to distinguish between a group (a Type with some structure) and the group viewed as a subgroup of itself.

The only additional aspect of “sets” we need to explain is that sets/subsets of X correspond to arrows X → Prop.