Type theory is an interdisciplinary field that connects the foundations of mathematics, programming languages, and proof verification. In this book, Benno van den Berg (ILLC) and Eric Faber develop a geometric interpretation of type theory based on a novel constructive theory of simplicial sets, a well-known geometric structure. This interpretation enables the development of new programming and proof techniques.
This book aligns with the exciting trend known as 'homotopy type theory', where geometry is utilized to develop new fundamental mathematical theories and algorithms. The contributions of Fields Medalist Vladimir Voevodsky have been essential to this field.