Roughly speaking, a type is a specification of its possible values.
- A value is some concrete thing, and a type is a collection of concrete things (but is itself not a concrete thing. For example any individual integer is a value, but the collection of all integers is a type. Much like elements and sets in set theory.
- A type is a collection of values which inhabit that type. A type is a value which is a member of the type of types.
- Type theory goes much much further than just tagging data.
- The type determines which data structure you use.
- Dependent types is basically about being able to express arbitrary things in your type system, meaning that you can construct arbitrary proofs. That's how Coq, Agda and Idris work.
- Types are types and propositions are propositions; types come from programming languages, and propositions from logic, and they seem to have no relation to each other.
- Learn TT - A collection of resources for learning type theory and type theory adjacent fields.
- Homotopy Type Theory lecture materials
- A textbook on informal homotopy type theory
- Homotopy type theory book
- GHOTL Project scope and outline plan - Good read.
- What I wish I knew when learning HoTT
- Collected works of Per Martin-Löf
- Type Theory: Does understanding of the Curry-Howard correspondence make you a better programmer?