to: create a context add an assumption to the context ("weakening") rearrange the assumptions use an assumption to create a variable define reflexivity, symmetry and transitivity for judgemental equality define substitution for application of lambda terms all the interactions of equality, substitution, etc. define universes Also, for each "by rule" type, there are 4 different kinds of rules "type formation" rules say how to create the type "term introduction" rules define the canonical terms and constructor functions, like "pair" and "S". "term elimination" rules define the other functions like "first", "second", and "R". "computation" rules specify how computation is performed with the type-specific functions. Examples of rules: Rules to Martin-Löf's Intuitionistic Type Theory Appendix A.2 of Homotopy Type Theory book Properties of type theories Terms usually belong to a single type. However, there are set theories that define "subtyping". Computation takes place by repeated application of rules. Many type theories are strongly normalizing, which means that any order of applying the rules will always end in the same result. However, some are not. In a normalizing type theory, the one-directional computation rules are called "reduction rules" and applying the rules "reduces" the term. If a rule is not one-directional, it is called a "conversion rule". Some combinations of types are equivalent to other combinations of types. When functions are considered "exponentiation", the combinations of types can be written similar to algebraic identities. Thus, , , , , . Axioms Most type theories do not have axioms. This is because a type theory is defined by its rules of inference. (See "Rules" above). This is a source of confusion for people familiar with Set Theory, where a theory is defined by both the rules of inference for a logic (such as first-order logic) and axioms about sets. Sometimes, a type theory will add a few axioms. An axiom is a judgement that is accepted without a derivation using the rules of inference. They are often added to ensure properties that cannot be added cleanly through the rules. Axioms can cause problems if they introduce terms without a way to compute on those terms. That is, axioms can interfere with the normalizing property of the type theory. Some commonly encountered axioms are: "Axiom K" ensures "uniqueness of identity proofs". That is, that every term of an identity type is equal to reflexivity. "Univalence Axiom" holds that equivalence of types is equality of