[<<][math][>>][..]

Fri Jul 5 18:26:55 EDT 2018

## intuitionistic type theory

Going over the wikipedia page
https://en.wikipedia.org/wiki/Intuitionistic_type_theory
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?

[Reply][About]

[<<][math][>>][..]