Fri Jul 5 18:26:55 EDT 2018
intuitionistic type theory
Going over the wikipedia page
What I miss in that page is a bit more of a direction. Clearly I'm
expecting something else than what is exposed...
I get the 3 primitive types: Bottom, Unit and bool.
But the type constructors are a little strange to me. Especially why
the Sigma is defined in terms of products.
Also, it says that dependent types model predicate logic. How?