Logic / Type theory

Some self-reflection (e.g., universe levels), but often needs a meta-system

Related to category theory via Curry–Howard–Lambek