"First class types" and "dependent types" are actually two different things. We can have first class types without any dependencies. For example: isEven :

"First class types" and "dependent types" are actually two different things. We can have first class types without any dependencies. For example: isEven : Nat -> Type isEven zero = Unit isEven (succ zero) = Empty isEven (succ (succ n)) = isEven n fortyTwoEven : isEven 42 fortyTwoEven = unit Here the `isEven` function calculates a type based on the given number: if the number's even, it returns the `Unit` type, of which there is a value `unit`; if the number's odd, it returns the `Empty` type, of which there are no values. The value `fortyTwoEven` is a "proof" that the number `42` (which would actually be `succ (succ (succ ...))` nested 42 times) is even. The proof is the value `unit`, which will only work if `isEven 42` returns `Unit`, which will only happen if 42 is even, so everything works out. We can write a type like `isEven 43`, but that will return the type `Empty`, which there's no way to satisfy. We can use this sort of thing to do static checks of reasonably simple data; for example, if we have a bunch of config parameters which need to be related in some way. Dependent types add the "naming" part, which we can use in functions (as explained above), but also in other "compound" datastructures like tuples `(n : Nat, isEven n)` and records `{ n : Nat, evenProof : isEven n }` The annoying thing is that few languages seem to have first class types at all, so every explanation of dependent types has to start by introducing first class types, and then explaining the "dependent" parts. It's like trying to explain something like interfaces, if all mainstream languages were dynamically typed. We'd have to begin by explaining what types are, and then go on to explain interfaces. Readers might easily confuse features of types with features of interfaces, which would lead to much confusion. I think that's kind of happened with "dependent types" and "first class types", although I haven't seen any/many systems which have one without the other, so maybe it's not too bad :)