タイプ・ライター その１

Advent Calendarも今日で折り返しとなりました．
今までに10以上の記事が載ってますが，他の参加者の方々の記事の内容がさっぱりわかりません．
ということで，私は基本的なことを記事にしてみました．
タイプについて，そもそもタイプとは？といったところから排除定理までを簡単に，また例を通じて考えてみようと思います．
本当は排除定理を使った例まで挙げたかったんですが，そこまでかけませんでした…．
追記：例まで挙げたものにしました．