Extends simple types with dependent functions, dependent pairs, inductive families, universes, and identity types. Learners encode specifications whose types carry precise mathematical guarantees.
