TTyped: A Simple Dependently Typed PL

TTyped is a simple dependently typed programming language based on the Calculus of Constructions. I designed it for academic purposes and demonstrate it's capabilities here in the hope that others will learn from it.

[spherinder]

Cool! This would be perfect for people learning type theory. I feel like languages like idris obfuscate the underlying concepts of their type systems with syntactic sugar. Although fundamentally there are only a handful of simple constructs to learn, which describe morphisms from type -> type, type -> value, value -> type, value -> value.