# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1672705703 -32400
# Node ID e086a266c6b75debb1cec938da5f41f600d9af97
# Parent  5b0525cb9a5df2a8383fd9fc1f038c4bac783036
FIP fix

diff -r 5b0525cb9a5d -r e086a266c6b7 src/LEMC.agda
--- a/src/LEMC.agda	Mon Jan 02 10:15:20 2023 +0900
+++ b/src/LEMC.agda	Tue Jan 03 09:28:23 2023 +0900
@@ -2,7 +2,7 @@
 open import Ordinals
 open import logic
 open import Relation.Nullary
-module LEMC {n : Level } (O : Ordinals {n} ) (p∨¬p : ( p : Set n) → p ∨ ( ¬ p )) where
+module LEMC {n : Level } (O : Ordinals {n} )  where
 
 open import zf
 open import Data.Nat renaming ( zero to Zero ; suc to Suc ;  ℕ to Nat ; _⊔_ to _n⊔_ ) 
@@ -32,6 +32,9 @@
 
 open HOD
 
+postulate 
+   p∨¬p : ( p : Set n) → p ∨ ( ¬ p ) 
+
 decp : ( p : Set n ) → Dec p   -- assuming axiom of choice    
 decp  p with p∨¬p p
 decp  p | case1 x = yes x
@@ -42,11 +45,16 @@
 ∋-p A x | case1 t  = yes t
 ∋-p A x | case2 t  = no (λ x → t x)
 
-double-neg-eilm : {A : Set n} → ¬ ¬ A → A      -- we don't have this in intutionistic logic
-double-neg-eilm  {A} notnot with decp  A                         -- assuming axiom of choice
+double-neg-elim : {A : Set n} → ¬ ¬ A → A      -- we don't have this in intutionistic logic
+double-neg-elim  {A} notnot with decp  A                         -- assuming axiom of choice
 ... | yes p = p
 ... | no ¬p = ⊥-elim ( notnot ¬p )
 
+-- by-contradiction : {A : Set n} {B : A → Set n}  → ¬ ( (a : A ) → ¬ B a ) → A    
+-- by-contradiction {A} {B} not with p∨¬p A         
+-- ... | case2 ¬a  = ⊥-elim (not (λ a → ⊥-elim (¬a a  )))          
+-- ... | case1 a = a            
+
 power→⊆ :  ( A t : HOD) → Power A ∋ t → t ⊆ A
 power→⊆ A t  PA∋t t∋x = subst (λ k → odef A k ) &iso ( t1 (subst (λ k → odef t k ) (sym &iso) t∋x))  where
    t1 : {x : HOD }  → t ∋ x → A ∋ x
diff -r 5b0525cb9a5d -r e086a266c6b7 src/ODC.agda
--- a/src/ODC.agda	Mon Jan 02 10:15:20 2023 +0900
+++ b/src/ODC.agda	Tue Jan 03 09:28:23 2023 +0900
@@ -4,9 +4,9 @@
 module ODC {n : Level } (O : Ordinals {n} ) where
 
 open import zf
-open import Data.Nat renaming ( zero to Zero ; suc to Suc ;  ℕ to Nat ; _⊔_ to _n⊔_ ) 
+open import Data.Nat renaming ( zero to Zero ; suc to Suc ;  ℕ to Nat ; _⊔_ to _n⊔_ )
 open import  Relation.Binary.PropositionalEquality
-open import Data.Nat.Properties 
+open import Data.Nat.Properties
 open import Data.Empty
 open import Relation.Nullary
 open import Relation.Binary
@@ -35,9 +35,9 @@
 
 open _∧_
 
-postulate      
+postulate
   -- mimimul and x∋minimal is an Axiom of choice
-  minimal : (x : HOD  ) → ¬ (x =h= od∅ )→ HOD 
+  minimal : (x : HOD  ) → ¬ (x =h= od∅ )→ HOD
   -- this should be ¬ (x =h= od∅ )→ ∃ ox → x ∋ Ord ox  ( minimum of x )
   x∋minimal : (x : HOD  ) → ( ne : ¬ (x =h= od∅ ) ) → odef x ( & ( minimal x ne ) )
   -- minimality (proved by ε-induction with LEM)
@@ -51,7 +51,7 @@
 
 pred-od :  ( p : Set n )  → HOD
 pred-od  p  = record { od = record { def = λ x → (x ≡ o∅) ∧ p } ;
-   odmax = osuc o∅; <odmax = λ x → subst (λ k →  k o< osuc o∅) (sym (proj1 x)) <-osuc } 
+   odmax = osuc o∅; <odmax = λ x → subst (λ k →  k o< osuc o∅) (sym (proj1 x)) <-osuc }
 
 ppp :  { p : Set n } { a : HOD  } → pred-od p ∋ a → p
 ppp  {p} {a} d = proj2 d
@@ -59,32 +59,32 @@
 p∨¬p : ( p : Set n ) → p ∨ ( ¬ p )         -- assuming axiom of choice
 p∨¬p  p with is-o∅ ( & (pred-od p ))
 p∨¬p  p | yes eq = case2 (¬p eq) where
-   ps = pred-od p 
-   eqo∅ : ps =h=  od∅  → & ps ≡  o∅  
-   eqo∅ eq = subst (λ k → & ps ≡ k) ord-od∅ ( cong (λ k → & k ) (==→o≡ eq)) 
+   ps = pred-od p
+   eqo∅ : ps =h=  od∅  → & ps ≡  o∅
+   eqo∅ eq = subst (λ k → & ps ≡ k) ord-od∅ ( cong (λ k → & k ) (==→o≡ eq))
    lemma : ps =h= od∅ → p → ⊥
    lemma eq p0 = ¬x<0  {& ps} (eq→ eq record { proj1 = eqo∅ eq ; proj2 = p0 } )
    ¬p : (& ps ≡ o∅) → p → ⊥
    ¬p eq = lemma ( subst₂ (λ j k → j =h=  k ) *iso o∅≡od∅ ( o≡→== eq ))
 p∨¬p  p | no ¬p = case1 (ppp  {p} {minimal ps (λ eq →  ¬p (eqo∅ eq))} lemma) where
-   ps = pred-od p 
-   eqo∅ : ps =h=  od∅  → & ps ≡  o∅  
-   eqo∅ eq = subst (λ k → & ps ≡ k) ord-od∅ ( cong (λ k → & k ) (==→o≡ eq)) 
-   lemma : ps ∋ minimal ps (λ eq →  ¬p (eqo∅ eq)) 
+   ps = pred-od p
+   eqo∅ : ps =h=  od∅  → & ps ≡  o∅
+   eqo∅ eq = subst (λ k → & ps ≡ k) ord-od∅ ( cong (λ k → & k ) (==→o≡ eq))
+   lemma : ps ∋ minimal ps (λ eq →  ¬p (eqo∅ eq))
    lemma = x∋minimal ps (λ eq →  ¬p (eqo∅ eq))
 
-decp : ( p : Set n ) → Dec p   -- assuming axiom of choice    
+decp : ( p : Set n ) → Dec p   -- assuming axiom of choice
 decp  p with p∨¬p p
 decp  p | case1 x = yes x
 decp  p | case2 x = no x
 
-∋-p : (A x : HOD ) → Dec ( A ∋ x ) 
+∋-p : (A x : HOD ) → Dec ( A ∋ x )
 ∋-p A x with p∨¬p ( A ∋ x ) -- LEM
 ∋-p A x | case1 t  = yes t
 ∋-p A x | case2 t  = no (λ x → t x)
 
-double-neg-eilm : {A : Set n} → ¬ ¬ A → A      -- we don't have this in intutionistic logic
-double-neg-eilm  {A} notnot with decp  A                         -- assuming axiom of choice
+double-neg-elim : {A : Set n} → ¬ ¬ A → A      -- we don't have this in intutionistic logic
+double-neg-elim  {A} notnot with decp  A                         -- assuming axiom of choice
 ... | yes p = p
 ... | no ¬p = ⊥-elim ( notnot ¬p )
 
@@ -95,6 +95,18 @@
 or-exclude {A} {B} (case2 b) | case1 a = case1 a
 or-exclude {A} {B} (case2 b) | case2 ¬a = case2 ⟪ ¬a , b ⟫
 
+-- record By-contradiction (A : Set n) (B : A → Set n)  : Set (suc n) where
+--  field
+--     a : A
+--     b : B a
+-- 
+-- by-contradiction : {A : Set n} {B : A → Set n}  → ¬ ( (a : A ) → ¬ B a ) → By-contradiction A B
+-- by-contradiction {A} {B} not with p∨¬p A 
+-- ... | case2 ¬a  = ⊥-elim (not (λ a → ⊥-elim (¬a a  )))
+-- ... | case1 a with p∨¬p (B a)
+-- ... | case1 b  = record { a = a ; b = b }
+-- ... | case2 ¬b = ⊥-elim ( not ( λ a b → ⊥-elim ( ¬b ? )))
+-- 
 power→⊆ :  ( A t : HOD) → Power A ∋ t → t ⊆ A
 power→⊆ A t  PA∋t tx = subst (λ k → odef A k ) &iso ( power→ A t PA∋t (subst (λ k → odef t k) (sym &iso) tx ) )
 
@@ -112,10 +124,10 @@
 open import zfc
 
 HOD→ZFC : ZFC
-HOD→ZFC   = record { 
-    ZFSet = HOD 
-    ; _∋_ = _∋_ 
-    ; _≈_ = _=h=_ 
+HOD→ZFC   = record {
+    ZFSet = HOD
+    ; _∋_ = _∋_
+    ; _≈_ = _=h=_
     ; ∅  = od∅
     ; Select = Select
     ; isZFC = isZFC
@@ -128,9 +140,9 @@
        choice = choice
      } where
          -- Axiom of choice ( is equivalent to the existence of minimal in our case )
-         -- ∀ X [ ∅ ∉ X → (∃ f : X → ⋃ X ) → ∀ A ∈ X ( f ( A ) ∈ A ) ] 
+         -- ∀ X [ ∅ ∉ X → (∃ f : X → ⋃ X ) → ∀ A ∈ X ( f ( A ) ∈ A ) ]
          choice-func : (X : HOD  ) → {x : HOD } → ¬ ( x =h= od∅ ) → ( X ∋ x ) → HOD
          choice-func X {x} not X∋x = minimal x not
-         choice : (X : HOD  ) → {A : HOD } → ( X∋A : X ∋ A ) → (not : ¬ ( A =h= od∅ )) → A ∋ choice-func X not X∋A 
+         choice : (X : HOD  ) → {A : HOD } → ( X∋A : X ∋ A ) → (not : ¬ ( A =h= od∅ )) → A ∋ choice-func X not X∋A
          choice X {A} X∋A not = x∋minimal A not
 
diff -r 5b0525cb9a5d -r e086a266c6b7 src/Topology.agda
--- a/src/Topology.agda	Mon Jan 02 10:15:20 2023 +0900
+++ b/src/Topology.agda	Tue Jan 03 09:28:23 2023 +0900
@@ -141,17 +141,23 @@
 
 -- covers
 
-record _covers_ ( P q : HOD  ) : Set (suc n) where
+record _covers_ ( P q : HOD  ) : Set n where
    field
-       cover   : {x : HOD} → q ∋ x → HOD
-       P∋cover : {x : HOD} → {lt : q ∋ x} → P ∋ cover lt
-       isCover : {x : HOD} → {lt : q ∋ x} → cover lt ∋ x
+       cover   : {x : Ordinal } → odef q x → Ordinal
+       P∋cover : {x : Ordinal } → {lt : odef q  x} → odef P (cover lt)
+       isCover : {x : Ordinal } → {lt : odef q  x} → odef (* (cover lt))  x
+
+open _covers_
 
 -- Finite Intersection Property
 
-record FIP {L : HOD} (top : Topology L) : Set (suc n) where
+record FIP {L : HOD} (top : Topology L) : Set n where
    field
-       fip≠φ : { C : HOD } { x : Ordinal } → C ⊆ CS top → Subbase C x → o∅ o< x 
+       finite : {X : Ordinal } → * X ⊆ CS top 
+          →       ( { C : Ordinal  } { x : Ordinal } → * C ⊆ * X → Subbase (* C) x → o∅ o< x ) →  Ordinal
+       limit : {X : Ordinal } → (CX : * X ⊆ CS top )
+          → ( fip : { C : Ordinal  } { x : Ordinal } → * C ⊆ * X → Subbase (* C) x → o∅ o< x ) 
+          →  {x : Ordinal } → odef (* X) x → odef (* x) (finite CX fip)
 
 -- Compact
 
@@ -159,20 +165,36 @@
    fin-e : {x : Ordinal } → odef S x → Finite-∪ S x
    fin-∪  : {x y : Ordinal } → Finite-∪ S x → Finite-∪ S y → Finite-∪ S (& (* x ∪ * y))
 
-record Compact  {L : HOD} (top : Topology L)  : Set (suc n) where
+record Compact  {L : HOD} (top : Topology L)  : Set n where
    field
-       finCover  : {X : HOD} → X ⊆ OS top → X covers L → HOD
-       isCover   : {X : HOD} → (xo : X ⊆ OS top) → (xcp : X covers L ) → (finCover xo xcp ) covers L
-       isFinite  : {X : HOD} → (xo : X ⊆ OS top) → (xcp : X covers L ) → Finite-∪ X (& (finCover xo xcp  ) )
+       finCover  : {X : Ordinal } → (* X) ⊆ OS top → (* X) covers L → Ordinal
+       isCover   : {X : Ordinal } → (xo : (* X) ⊆ OS top) → (xcp : (* X) covers L ) → (* (finCover xo xcp )) covers L
+       isFinite  : {X : Ordinal } → (xo : (* X) ⊆ OS top) → (xcp : (* X) covers L ) → Finite-∪ (* X) (finCover xo xcp ) 
 
 -- FIP is Compact
 
 FIP→Compact : {L : HOD} → (top : Topology L ) → FIP top  → Compact top
-FIP→Compact {L} top fip = record { finCover = finCover ; isCover = ? ; isFinite = ? } where
-    finCover  : {C : HOD} → C ⊆ OS top → C covers L → HOD
-    finCover {C} C<T CL = record { od = record { def = λ x → odef L x ∧ ( ¬ Subbase C x) } ; odmax = & L ; <odmax = odef∧< }
-    isConver : {C : HOD} (xo : C ⊆ OS top) (xcp : C covers L) → (finCover xo xcp) covers L
-    isConver {C} xo xcp = record { cover = λ lx → ? ; P∋cover = ? ; isCover = ? }
+FIP→Compact {L} top fip = record { finCover = finCover ; isCover = isCover1 ; isFinite = isFinite } where
+   remain : {X : Ordinal } → (* X) ⊆ OS top → ¬ ( (* X) covers L ) → Ordinal 
+   remain = ?
+   remain-is-intersection : {X : Ordinal } → (ox : (* X) ⊆ OS top) → (r : ¬ ( (* X) covers L ) )
+       →  {x : Ordinal } → odef (* X) x → odef (L ＼ * x ) (remain ox r)
+   -- HOD of a counter example of fip 
+   tp00 : {X : Ordinal} → * X ⊆ OS top → HOD
+   tp00 {X} ox = record { od = record { def = λ x → { C : Ordinal  } → * C ⊆ * X → Subbase (L ＼ * C) x }
+       ; odmax = & L ; <odmax = ? }
+   finCover :  {X : Ordinal} → * X ⊆ OS top → * X covers L → Ordinal
+   finCover {X} ox oc = ? where
+        -- X is the counter example of fip
+        tp01 : {x : Ordinal } → odef (L ＼  * X) ( FIP.finite fip ? ?  ) → odef (* x) ( FIP.finite fip ? ?  )
+        tp01 {x} P = FIP.limit fip ? ? ? 
+   -- yes, it is finite
+   isFinite : {X : Ordinal} (xo : * X ⊆ OS top) (xcp : * X covers L) → Finite-∪ (* X) (finCover xo xcp)
+   isFinite = ?
+   -- is also a cover
+   isCover1 : {X : Ordinal} (xo : * X ⊆ OS top) (xcp : * X covers L) → * (finCover xo xcp) covers L
+   isCover1 = ?
+
 
 Compact→FIP : {L : HOD} → (top : Topology L ) → Compact top  → FIP top
 Compact→FIP = {!!}