誰か比喩って言った？
型理論において、「型」は「命題」、「型Aから型Bへの写像を記述するブログラム」は「『命題A⇒命題B』の証明」に対応。