### diff OD.agda @ 271:2169d948159b

fix incl
author Shinji KONO Mon, 30 Dec 2019 23:45:59 +0900 53744836020b 985a1af11bce
line wrap: on
line diff
```--- a/OD.agda	Mon Oct 07 01:28:11 2019 +0900
+++ b/OD.agda	Mon Dec 30 23:45:59 2019 +0900
@@ -36,16 +36,17 @@
id : {A : Set n} → A → A
id x = x

-eq-refl :  {  x :  OD  } → x == x
-eq-refl  {x} = record { eq→ = id ; eq← = id }
+==-refl :  {  x :  OD  } → x == x
+==-refl  {x} = record { eq→ = id ; eq← = id }

open  _==_

-eq-sym :  {  x y :  OD  } → x == y → y == x
-eq-sym eq = record { eq→ = eq← eq ; eq← = eq→ eq }
+==-trans : { x y z : OD } →  x == y →  y == z →  x ==  z
+==-trans x=y y=z  = record { eq→ = λ {m} t → eq→ y=z (eq→ x=y t) ; eq← =  λ {m} t → eq← x=y (eq← y=z t) }

-eq-trans :  {  x y z :  OD  } → x == y → y == z → x == z
-eq-trans x=y y=z = record { eq→ = λ t → eq→ y=z ( eq→ x=y  t) ; eq← = λ t → eq← x=y ( eq← y=z t) }
+==-sym : { x y  : OD } →  x == y →  y == x
+==-sym x=y = record { eq→ = λ {m} t → eq← x=y t ; eq← =  λ {m} t → eq→ x=y t }
+

⇔→== :  {  x y :  OD  } → ( {z : Ordinal } → def x z ⇔  def y z) → x == y
eq→ ( ⇔→==  {x} {y}  eq ) {z} m = proj1 eq m
@@ -74,7 +75,7 @@
-- next assumption causes ∀ x ∋ ∅ . It menas only an ordinal is allowed as OD
--   o<→c<  : {n : Level} {x y : Ordinal  } → x o< y → def (ord→od y) x
--   ord→od x ≡ Ord x results the same
-  -- supermum as Replacement Axiom
+  -- supermum as Replacement Axiom ( this assumes Ordinal has some upper bound )
sup-o  :  ( Ordinal  → Ordinal ) →  Ordinal
sup-o< :  { ψ : Ordinal  →  Ordinal } → ∀ {x : Ordinal } → ψ x  o<  sup-o ψ
-- contra-position of mimimulity of supermum required in Power Set Axiom
@@ -140,10 +141,10 @@
ord→== : { x y : OD  } → od→ord x ≡  od→ord y →  x == y
ord→==  {x} {y} eq = ==-iso (lemma (od→ord x) (od→ord y) (orefl eq)) where
lemma : ( ox oy : Ordinal  ) → ox ≡ oy →  (ord→od ox) == (ord→od oy)
-   lemma ox ox  refl = eq-refl
+   lemma ox ox  refl = ==-refl

o≡→== : { x y : Ordinal  } → x ≡  y →  ord→od x == ord→od y
-o≡→==  {x} {.x} refl = eq-refl
+o≡→==  {x} {.x} refl = ==-refl

o∅≡od∅ : ord→od (o∅ ) ≡ od∅
o∅≡od∅  = ==→o≡ lemma where
@@ -162,7 +163,7 @@
eq← ∅0 {w} lt = lift (¬x<0 lt)

∅< : { x y : OD  } → def x (od→ord y ) → ¬ (  x  == od∅  )
-∅<  {x} {y} d eq with eq→ (eq-trans eq (eq-sym ∅0) ) d
+∅<  {x} {y} d eq with eq→ (==-trans eq (==-sym ∅0) ) d
∅<  {x} {y} d eq | lift ()

∅6 : { x : OD  }  → ¬ ( x ∋ x )    --  no Russel paradox
@@ -191,12 +192,6 @@
right (case1 t) = case2 t
right (case2 t) = case1 t

-==-trans : { x y z : OD } →  x == y →  y == z →  x ==  z
-==-trans x=y y=z  = record { eq→ = λ {m} t → eq→ y=z (eq→ x=y t) ; eq← =  λ {m} t → eq← x=y (eq← y=z t) }
-
-==-sym : { x y  : OD } →  x == y →  y == x
-==-sym x=y = record { eq→ = λ {m} t → eq← x=y t ; eq← =  λ {m} t → eq→ x=y t }
-
ord≡→≡ : { x y : OD } → od→ord x ≡ od→ord y → x ≡ y
ord≡→≡ eq = subst₂ (λ j k → j ≡ k ) oiso oiso ( cong ( λ k → ord→od k ) eq )

@@ -339,15 +334,21 @@
Def :  (A :  OD ) → OD
Def  A = Ord ( sup-o  ( λ x → od→ord ( ZFSubset A (ord→od x )) ) )

-_⊆_ :  ( A B : OD   ) → ∀{ x : OD  } →  Set n
-_⊆_ A B {x} = A ∋ x →  B ∋ x
+-- _⊆_ :  ( A B : OD   ) → ∀{ x : OD  } →  Set n
+-- _⊆_ A B {x} = A ∋ x →  B ∋ x
+
+record _⊆_ ( A B : OD   ) : Set (suc n) where
+  field
+     incl : { x : OD } → A ∋ x →  B ∋ x
+
+open _⊆_

infixr  220 _⊆_

-subset-lemma : {A x y : OD  } → (  x ∋ y → ZFSubset A x ∋  y ) ⇔  ( _⊆_ x A {y} )
-subset-lemma  {A} {x} {y} = record {
-      proj1 = λ z lt → proj1 (z  lt)
-    ; proj2 = λ x⊆A lt → record { proj1 = x⊆A lt ; proj2 = lt }
+subset-lemma : {A x : OD  } → ( {y : OD } →  x ∋ y → ZFSubset A x ∋  y ) ⇔  ( x ⊆ A  )
+subset-lemma  {A} {x} = record {
+      proj1 = λ lt  → record { incl = λ x∋z → proj1 (lt x∋z)  }
+    ; proj2 = λ x⊆A lt → record { proj1 = incl x⊆A lt ; proj2 = lt }
}

open import Data.Unit
@@ -406,7 +407,7 @@
-- infixr  230 _∩_ _∪_
isZF : IsZF (OD )  _∋_  _==_ od∅ _,_ Union Power Select Replace infinite
isZF = record {
-           isEquivalence  = record { refl = eq-refl ; sym = eq-sym; trans = eq-trans }
+           isEquivalence  = record { refl = ==-refl ; sym = ==-sym; trans = ==-trans }
;   pair→  = pair→
;   pair←  = pair←
;   union→ = union→
@@ -436,14 +437,14 @@
empty : (x : OD  ) → ¬  (od∅ ∋ x)
empty x = ¬x<0

-         o<→c< :  {x y : Ordinal } {z : OD }→ x o< y → _⊆_  (Ord x) (Ord y) {z}
-         o<→c< lt lt1 = ordtrans lt1 lt
+         o<→c< :  {x y : Ordinal } → x o< y → (Ord x) ⊆ (Ord y)
+         o<→c< lt = record { incl = λ z → ordtrans z lt }

-         ⊆→o< :  {x y : Ordinal } → (∀ (z : OD) → _⊆_  (Ord x) (Ord y) {z} ) →  x o< osuc y
+         ⊆→o< :  {x y : Ordinal } → (Ord x) ⊆ (Ord y) →  x o< osuc y
⊆→o< {x} {y}  lt with trio< x y
⊆→o< {x} {y}  lt | tri< a ¬b ¬c = ordtrans a <-osuc
⊆→o< {x} {y}  lt | tri≈ ¬a b ¬c = subst ( λ k → k o< osuc y) (sym b) <-osuc
-         ⊆→o< {x} {y}  lt | tri> ¬a ¬b c with lt (ord→od y) (o<-subst c (sym diso) refl )
+         ⊆→o< {x} {y}  lt | tri> ¬a ¬b c with (incl lt)  (o<-subst c (sym diso) refl )
... | ttt = ⊥-elim ( o<¬≡ refl (o<-subst ttt diso refl ))

union→ :  (X z u : OD) → (X ∋ u) ∧ (u ∋ z) → Union X ∋ z
@@ -551,15 +552,15 @@
lemma6 : od→ord t ≡ od→ord (A ∩ ord→od (od→ord t))
lemma6 = cong ( λ k → od→ord k ) (==→o≡ (subst (λ k → t == (A ∩ k)) (sym oiso) ( ∩-≡ t→A  )))

-         ord⊆power : (a : Ordinal) → (x : OD) → _⊆_ (Ord (osuc a)) (Power (Ord a)) {x}
-         ord⊆power a x lt = power← (Ord a) x lemma where
-                lemma : {y : OD} → x ∋ y → Ord a ∋ y
-                lemma y<x with osuc-≡< lt
-                lemma y<x | case1 refl = c<→o< y<x
-                lemma y<x | case2 x<a = ordtrans (c<→o< y<x) x<a
+         ord⊆power : (a : Ordinal) → (Ord (osuc a)) ⊆ (Power (Ord a))
+         ord⊆power a = record { incl = λ {x} lt →  power← (Ord a) x (lemma lt) } where
+                lemma : {x y : OD} → od→ord x o< osuc a → x ∋ y →  Ord a ∋ y
+                lemma lt y<x with osuc-≡< lt
+                lemma lt y<x | case1 refl = c<→o< y<x
+                lemma lt y<x | case2 x<a = ordtrans (c<→o< y<x) x<a

-         -- continuum-hyphotheis : (a : Ordinal) → (x : OD) → _⊆_  (Power (Ord a)) (Ord (osuc a)) {x}
-         -- continuum-hyphotheis a x = ?
+         -- continuum-hyphotheis : (a : Ordinal) → Power (Ord a) ⊆ Ord (osuc a)
+         -- continuum-hyphotheis a = ?

--  assuming axiom of choice
regularity :  (x : OD) (not : ¬ (x == od∅)) →
@@ -620,12 +621,12 @@
lemma-ord : ( ox : Ordinal  ) → ψ ox
lemma-ord  ox = TransFinite {ψ} induction ox where
∋-p : (A x : OD ) → Dec ( A ∋ x )
-                    ∋-p A x with p∨¬p (Lift (suc n) ( A ∋ x ))
+                    ∋-p A x with p∨¬p (Lift (suc n) ( A ∋ x )) -- LEM
∋-p A x | case1 (lift t)  = yes t
∋-p A x | case2 t  = no (λ x → t (lift x ))
∀-imply-or :  {A : Ordinal  → Set n } {B : Set (suc n) }
→ ((x : Ordinal ) → A x ∨ B) →  ((x : Ordinal ) → A x) ∨ B
-                    ∀-imply-or  {A} {B} ∀AB with p∨¬p (Lift ( suc n ) ((x : Ordinal ) → A x))
+                    ∀-imply-or  {A} {B} ∀AB with p∨¬p (Lift ( suc n ) ((x : Ordinal ) → A x)) -- LEM
∀-imply-or  {A} {B} ∀AB | case1 (lift t) = case1 t
∀-imply-or  {A} {B} ∀AB | case2 x  = case2 (lemma (λ not → x (lift not ))) where
lemma : ¬ ((x : Ordinal ) → A x) →  B
@@ -643,8 +644,7 @@
lemma :  ((y : Ordinals.ord O) → (O Ordinals.o< y) x → def X y → ⊥) ∨ choiced X
lemma = ∀-imply-or lemma1
have_to_find : choiced X
-                 have_to_find with lemma-ord (od→ord X )
-                 have_to_find | t = dont-or  t ¬¬X∋x where
+                 have_to_find = dont-or  (lemma-ord (od→ord X )) ¬¬X∋x where
¬¬X∋x : ¬ ((x : Ordinal) → x o< (od→ord X) → def X x → ⊥)
¬¬X∋x nn = not record {
eq→ = λ {x} lt → ⊥-elim  (nn x (def→o< lt) lt) ```