I always get confused about terms, types, expressions, etc. in full spectrum dependent types… so toying around with these :sparkles: very informal :sparkles: Venn diagram thingies.
Note: Don't take this super seriously or authoritatively, it's more me trying to figure things out, and I'm very sloppy at this stuff!
term ::=
| var % variable
| Type % universe (type)
| Π (x : term). term % function former (type)
| λ (x : term). term % function introduction (expression)
| term term % function elimination (expression)
| ...
╭──────────────────────────────────────────────────────────────────────╮
│ Term │
│ │
│ ╭──────────────╮ │
│ │ Variable │ │
│ ╰──────────────╯ │
│ ╭────────────────────────╮ ╭───────────────────────────────────╮ │
│ │ Expression │ │ Type │ │
│ │ ╭─────────┬────────╮ │ │ ╭────────────╮ ╭────────────╮ │ │
│ │ │ Intro │ Elim │ │ ∈ │ │ Former │ ∈ │ Universe │ │ │
│ │ ╰─────────┴────────╯ │ │ ╰────────────╯ ╰────────────╯ │ │
│ ╰────────────────────────╯ ╰───────────────────────────────────╯ │
╰──────────────────────────────────────────────────────────────────────╯
value ::=
| stuck
| Type % universe (type)
| Π (x : value). ⟨value*, term⟩ % function former (type)
| λ (x : value). ⟨value*, term⟩ % function introduction (expression)
| ...
stuck ::=
| var % variable
| stuck term % function elimination (expression)
| ...
╭────────────────────────────────────────────────────────────────────────────────────╮
│ Value │
│ │
│ ╭────────────────────╮ │
│ │ Stuck (Neutral) │ │
│ │ │ │
│ │ ╭────────────╮ │ │
│ │ │ Variable │ │ │
│ │ ╰────────────╯ │ │
│ │ ╭───────────────────────────────────╮ ╭───────────────────────────────────╮ │
│ │ │ Expression │ │ Type │ │
│ │ │ ╭──────────╮ ╷ ╭────────────╮ │ │ ╭────────────╮ ╭────────────╮ │ │
│ │ │ │ Elim │ ╎ │ Intro │ │ ∈ │ │ Former │ ∈ │ Universe │ │ │
│ │ │ ╰──────────╯ ╎ ╰────────────╯ │ │ ╰────────────╯ ╰────────────╯ │ │
│ │ ╰───────────────────────────────────╯ ╰───────────────────────────────────╯ │
│ ╰────────────────────╯ │
╰────────────────────────────────────────────────────────────────────────────────────╯
Entity/Object
╭─────────────────────┬─────────────────────────────────────╮
│ │ │
│ Definition ∈ Declaration │
│ │ │
│ ╭────────────────────────────────────────╮ │
│ │ ╭───────────────╮ │ │ ∈ Context/Environment
│ │ Abstract │ Variable │ Opaque │ │
│ │ ╰───────────────╯ │ ╭────────╮ │
│ ├────────────────────────────────────────┤ ∈ │ Type │ │
│ │ ╭───────────────╮ │ ╰────────╯ │
│ │ Concrete │ Value │ Transparent │ │
│ │ ╰───────────────╯ │ │
│ ╰────────────────────────────────────────╯ │
╰─────────────────────┴─────────────────────────────────────╯