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?