diff options
| -rw-r--r-- | theories/Logic/ProofIrrelevance.v | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/theories/Logic/ProofIrrelevance.v b/theories/Logic/ProofIrrelevance.v index afdc0ffee3..7c8869d5d8 100644 --- a/theories/Logic/ProofIrrelevance.v +++ b/theories/Logic/ProofIrrelevance.v @@ -108,7 +108,8 @@ Proof End Proof_irrelevance_CCI. -(** Remark: in CCI, [bool] can be taken in [Set] as well in the - paradox and since [~true=false] for [true] and [false] in - [bool], we get the inconsistency of [em : forall A:Prop, {A}+{~A}] in CCI +(** Remark: in the Set-impredicative CCI, Hurkens' paradox still holds with + [bool] in [Set] and since [~true=false] for [true] and [false] + in [bool] from [Set], we get the inconsistency of + [em : forall A:Prop, {A}+{~A}] in the Set-impredicative CCI. *) |