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.

Roughly speaking, a type is a specification of its possible values.

Learn TT - A collection of resources for learning type theory and type theory adjacent fields.

GHOTL Project scope and outline plan - Good read.

Hazel - Live functional programming environment with typed holes.

LaTTe - Laboratory for Type Theory experiments (in clojure).

TT Lite - SuperCompiler for Martin-Löf's Type Theory.

SymmetryBook - Undergraduate textbook written in the univalent style, taking advantage of the presence of symmetry in the logic at an early stage.

nbe-for-mltt - Normalization by Evaluation for Martin-Löf Type Theory.

[Timeline for Logic, λ-Calculus, and Programming Language Theory (2012)(http://fm.csl.sri.com/SSFT15/Timeline.pages.pdf) (HN)

qtt - Quantitative Type Theory implementation.

mlsub - Prototype type inference engine.

PRL Project - Implementing computational mathematics and providing logic-based tools that help automate programming.