A Kotlin implementation of the First order dependent type theory as described in A tutorial implementation of a dependently typed lambda calculus by Andres Loh, Conor McBride and Wouter Swierstra
It has the implementation for Natural Numbers and length-perameterized vectors. As there is no way to have user defined data types, this is mostly usless, but a interesting look at the most basic implementation of dependant types.