Elementary Realm-Like Structures
| No | Variant 1 | Variant 2 | Variant 3 |
|---|---|---|---|
| 01 | f:A\to(B\to C) | f:A\times B\to C | |
| 02 | a:\mathcal P(A) | a:A\to\mathbb B | |
| 03 | f:A\rightharpoonup B |
f:A\to Maybe B
|
f:\mathcal P(A\times B) with \vdash"f is right-unique" |
| 04 | a:A | a:\mathcal P(A) with \vdash|a|=1 | a:\{*\}\to A |
| 05 | f:A\to B | f:A\to \mathcal P(B) with \vdash\forall x:A.|f(x)|=1 | f:\mathcal P(A\times B) with \vdash"f is left-total and right-unique" |
| 06 | \mathbb N starting with 0 | \mathbb N starting with 1 |
06 propagates to arrays/sequences/... whose indices start either with 0 or with 1