| | 159 | === Names === |
| | 160 | |
| | 161 | As an aside, note that we have to come up with names like `UU` and `KK` for the `Universe` |
| | 162 | even though we really just wanted to use `U1` and `K1`, like before. Then we would have |
| | 163 | a type and a constructor with the same name, but that's ok. However, `Universe` defines |
| | 164 | both a type (with constructors) and a kind (with types). So if we were to use `U1` in the |
| | 165 | `Universe` constructors, then we could no longer use that name in the `Interprt` |
| | 166 | constructors. It's a bit annoying, because we are never really interested in the type |
| | 167 | `Universe` and its constructors: we're only interested in its promoted variant. |
| | 168 | This is a slight annoyance of automatic promotion: when you define a "singleton type" |
| | 169 | (like our GADT `Interprt` for `Universe`) you cannot reuse the constructor names. |
| | 170 | Oh well. |
| | 171 | |
