This chapter introduces intuitionistic type theory, a foundational system for mathematics developed by Per Martin-Löf. The theory aims to address the limitations of classical logic and set theory, particularly in handling infinite domains and quantification over all sets. Martin-Löf explains the distinction between propositions and judgments, emphasizing that propositions are defined by their proofs and that truth is identified with provability. The chapter outlines the basic forms of judgment, including set formation, equality, membership, and equality of elements, and provides detailed rules for equality and hypothetical judgments. It also discusses the concept of categories and the relationship between types, sets, and categories. The chapter concludes with examples of combinatorial logic, such as the combinator \( I \) and \( K \), illustrating how intuitionistic type theory can be used to define and manipulate functions and propositions.This chapter introduces intuitionistic type theory, a foundational system for mathematics developed by Per Martin-Löf. The theory aims to address the limitations of classical logic and set theory, particularly in handling infinite domains and quantification over all sets. Martin-Löf explains the distinction between propositions and judgments, emphasizing that propositions are defined by their proofs and that truth is identified with provability. The chapter outlines the basic forms of judgment, including set formation, equality, membership, and equality of elements, and provides detailed rules for equality and hypothetical judgments. It also discusses the concept of categories and the relationship between types, sets, and categories. The chapter concludes with examples of combinatorial logic, such as the combinator \( I \) and \( K \), illustrating how intuitionistic type theory can be used to define and manipulate functions and propositions.