Mathematics in type theory
Constructing proof is an art, checking them is a science. Making a distinction between the statement of a theorem and the proof is important. It means that if we have a proof of P, we can make a proof of Q. It is a function from the proofs of P to the proofs of Q. It is a function sending an element of P to an element of Q. It is a term of type P → Q. …This is why in the natural number game we use the → symbol to denote implication.