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

changeset 301:b012a915bbb5

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
contradiction found ...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 24 Jun 2020 14:05:38 +0900
parents e70980bd80c7
children 304c271b3d47
files OD.agda filter.agda
diffstat 2 files changed, 8 insertions(+), 1 deletions(-) [+]
line wrap: on
line diff
--- a/OD.agda	Tue Jun 23 15:12:43 2020 +0900
+++ b/OD.agda	Wed Jun 24 14:05:38 2020 +0900
@@ -96,6 +96,11 @@
 maxod : {x : OD} → od→ord x o< od→ord Ords
 maxod {x} = c<→o< OneObj
 
+-- we have to avoid this contradiction
+
+bad-bad : ⊥
+bad-bad = osuc-< <-osuc (c<→o< { record { def = λ x → One }} OneObj)
+
 -- Ordinal in OD ( and ZFSet ) Transitive Set
 Ord : ( a : Ordinal  ) → OD 
 Ord  a = record { def = λ y → y o< a }  
--- a/filter.agda	Tue Jun 23 15:12:43 2020 +0900
+++ b/filter.agda	Wed Jun 24 14:05:38 2020 +0900
@@ -129,9 +129,11 @@
 
 --    the set of finite partial functions from ω to 2
 --
+--   ph2 : Nat → Set → 2
+--   ph2 : Nat → Maybe 2
+--
 -- Hω2 : Filter (Power (Power infinite))
 
-
 record Ideal  ( L : OD  ) : Set (suc n) where
    field
        ideal : OD