Coq.Logic にはCoqの集合論モデルにおいて正しい公理や、それらの間の関係が記述されている。ここではその一部を取り上げて、意味を説明する。 前提知識 公理を仮定しない状態では、 Coqの論理は直観主義論理である。 ある2つが「等しい」という命題が証明で…