# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1592975138 -32400
# Node ID b012a915bbb5a14c904ef34ed19742276689c4c6
# Parent  e70980bd80c76c7a021641dfa3628e502644738e
contradiction found ...

diff -r e70980bd80c7 -r b012a915bbb5 OD.agda
--- 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 }  
diff -r e70980bd80c7 -r b012a915bbb5 filter.agda
--- 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