Categorical proof theory studies the structure of propositions and deductions by representing them as objects and morphisms within a category. In this gentle introduction to categorical proof theory, we begin with an extensive overview of category theory itself, motivating some of its basic notions through numerous examples and proof-theoretic intuitions. We then introduce three families of categories—bicartesian closed, almost bicartesian closed, and cartesian closed—to serve as categorical formalizations of three fragments of intuitionistic propositional deduction. We also present presheaf categories as the categorical formalization of the Brouwer-Heyting-Kolmogorov (BHK) interpretation and provide some representation theorems illustrating the generality of the BHK reading of intuitionistic deductions. In addition, we briefly discuss certain aspects of categorical proof theory for classical propositional logic. Subsequently, we employ the aforementioned three families of categories as semantics for formal intuitionistic propositional deductions and establish soundness and completeness results for three fundamental problems: the existence of proofs, the equality of proofs, and the identity of propositions. Finally, we extend the discussion from propositional to higher-order languages, introduce a form of realizability, and use it to construct computable (resp. continuous) worlds in which all functions are computable (resp. continuous). These constructions enable us to prove the consistency of certain anti-classical theories, such as finite-type Heyting arithmetic with the Church-Turing Thesis or with Brouwer’s Continuity Principle. Moreover, realizability provides a means of extracting computational content from intuitionistic and classical arithmetical proofs. For instance, we show that any provably recursive function in Heyting or Peano arithmetic is a primitive recursive functional.