diff options
| author |  Arnaud Spiwack <arnaud@spiwack.net> | 2014-09-25 09:58:03 +0200 |
|---|---|---|
| committer | Arnaud Spiwack <arnaud@spiwack.net> | 2014-09-25 09:58:03 +0200 |
| commit | 31205e035316a7795ee3a1e0045148194cdcfcae (patch) | |
| tree | b1bef4bdce601e06afeb56b4b849a443008fa19a /theories/Logic | |
| parent | bec7e0914f4a7144cd4efa8ffaccc9f72dbdb790 (diff) | |
Hurkens.v: update comments.
Diffstat (limited to 'theories/Logic')
| -rw-r--r-- | theories/Logic/Hurkens.v | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/theories/Logic/Hurkens.v b/theories/Logic/Hurkens.v index 06c72a4cb..5f1d5232f 100644 --- a/theories/Logic/Hurkens.v +++ b/theories/Logic/Hurkens.v @@ -38,8 +38,11 @@ - The [NoRetractFromTypeToProp] module proves that [Prop] cannot be a retract of a larger type. - - The [Prop_neq_Type] module proves that [Prop] is different from - any larger [Type]. + - The [TypeNeqSmallType] module proves that [Type] is different + from any smaller type. + + - The [PropNeqType] module proves that [Prop] is different from + any larger [Type]. It is an instance of the previous result. References: |