「論理計算のための宇宙と型、二種類の述語」において、二元の宇宙 $`{\bf Prop}`$ を次のように定義しました。$`\quad {\bf Prop} := |{\bf Bool}|`$$`{\bf Bool}`$ は2つの対象 $`{\bf 0}, {\bf 1}`$ だけを持つ集合圏の充満部分圏です。しかし実際の証明…