This will be a lecture attempting to teach basic type theory, emphasizing the shared structure between collections (as in set theory) and propositions (as in logic). I will begin with the main idea and utility of type theory, then dive into inference rules, intuitionistic sequent calculus, typing rules, computation rules, and the propositions as types interpretation. If time allows, we can talk about dependent types and/or inductive types.