Rocqの世界
==========

このサイトは現在制作中です。

.. toctree::
   :maxdepth: 2
   :caption: Contents:

   about
   logic
   boolean
   classical_logic
   relation
   preorder
   power
   power_classical
   function
   unique_choice
   quotient
   finite
   finite_sequence
   category
   functor
   topological_space
   partial_function
   pointed_type
   first_order_logic
   recursion_theory

使用する公理
------------

* 初等トポスで成り立つ公理は自由に使う（このとき ``Prop`` は部分対象分類子と見なす）。

  * たとえば、function extensionalityやpropositional extensionality、definite descriptionや一意選択、そして ``P : Prop`` に対するproof irrelevanceなどである。

* 古典公理は、それを避けることが不便であるときは遠慮なく使う。

  * このとき、``P : Prop`` に対する排中律や2重否定除去などを使い、一般の ``A : Type`` に対する古典公理は使わない（後者は強い形の選択演算子のようなものであり、選択公理を含意してしまう）。

* 可算選択公理や従属選択公理は、必要なときに遠慮なく使う。

* 選択公理はそれが真に必要なときにしか使わない。

  * たとえばHahn—Banachの定理を示すときには使うだろうが、「Hausdorff空間のコンパクト部分集合が閉集合」であることを示すときには使わない（後者の典型的な証明は暗黙に選択公理を使っている）。