Type theory is a branch of mathematical logic and computer science that deals with the classification of entities into types. It serves as a framework for formalizing reasoning about programs and mathematical propositions, providing a foundation for understanding and manipulating both data and functions. Here are some key aspects of type theory: 1. **Types as a Foundation**: In type theory, everything has a type, which describes the nature of a value or expression.
Alternative to set theory, and some say it is better for proof assistants, and many of the most popular proof assistants of the 2020s use it e.g. Lean and Coq.
New to topics? Read the docs here!