Mercurial > hg > Members > kono > Proof > ZF-in-agda

diff OD.agda @ 346:06f10815d0b3

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 13 Jul 2020 19:19:02 +0900
parents e0916a632971
children 08d94fec239c
line wrap: on
line diff
--- a/OD.agda	Mon Jul 13 14:46:03 2020 +0900
+++ b/OD.agda	Mon Jul 13 19:19:02 2020 +0900
@@ -376,7 +376,7 @@
     -- We simply assumes infinite-d y has a maximum.
     -- 
     -- This means that many of OD may not be HODs because of the od→ord mapping divergence.
-    -- We should have some axioms to prevent this.
+    -- We should have some axioms to prevent this such as od→ord x o< next (odmax x).
     -- 
     postulate
         ωmax : Ordinal