Much contemporary type theory research is based on formal type theory, which is defined by a collection of inference rules that are carefully chosen so as to admit a rich variety of interpretations in various mathematical and computational settings. Coq and its many derivatives are the prime examples of formal type theory in action. An alternative approach, pioneered in early work of Martin-Loef and developed to fruition by Constable, is computational type theory, which provides direct expression of the computational meaning of mathematics in the style of Brouwer. Computational type theory starts with a programming language and develops type theories defined by semantic, rather than syntactic conditions. One may say that computational type theory is a (Brouwerian) theory of truth, whereas formal type theory is a theory of proof. In these lectures we will develop the basic structure of computational type theory by providing a computational meaning explanation for typing, including the recently introduced concepts of higher-dimensional type theory.