>>14277730I forgot
I already been trying to understand curry howard isomorphism for some time,
I understood the idea of proposition encoded as types, implication as functions, AND as product type, OR as sum type.
But I had a little trouble with existential and universal quantifier (which have dependent types as counter part)
Then I've found this :
https://www.youtube.com/watch?v=FquVty-Ghpgwhich really shed sometime, so I'm diving in all this again with a new understanding
and it made me understand what the guy said in this one
https://www.youtube.com/watch?v=3WBUHEVr56cwhich is that Calculus of Consstruction (used in Coq) is basically
typed lambda calculus
+ functions from types to terms (parametric types, polymorphism)
+ functions from types to types (ex: list "function" in haskell, the list of types alpha (the input) is itself a type (the output))
+ functions from terms to types (dependent types) (like the type of lists of 3 elements)
