We will give some more strict Type Theory and Category Theory introduction in this chapter as it relates to Haskell. We will not focus on proofs too much (or at all) but will be providing (some) definitions and a hierarchy of concepts, which you can use as reference material as you delve deeper into the Haskell world. Strictly speaking, Haskell does not use the full intuitionistic Type Theory per se but is rather based on so-called System FC, or System F with coercions. The reasons for it are mainly that System FC, while being quite powerful (much more powerful than any imperative language), allows for fully deducible typechecking. This means you may omit writing type signatures altogether, and the compiler will deduce them for you. Try doing it in C# or Java.