Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 653:4186c0331abb
sind again
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Thu, 30 Jun 2022 06:57:05 +0900 |
| parents | cf5af048db99 |
| children | 6df8b836e983 |
| files | src/OrdUtil.agda src/ordinal.agda src/zorn.agda |
| diffstat | 3 files changed, 154 insertions(+), 178 deletions(-) [+] |
line wrap: on
line diff
--- a/src/OrdUtil.agda Sat Jun 25 17:36:18 2022 +0900 +++ b/src/OrdUtil.agda Thu Jun 30 06:57:05 2022 +0900 @@ -41,9 +41,6 @@ osuc-< {x} {y} y<ox x<y | case2 y<x = o<> x<y y<x osucc : {ox oy : Ordinal } → oy o< ox → osuc oy o< osuc ox ----- y < osuc y < x < osuc x ----- y < osuc y = x < osuc x ----- y < osuc y > x < osuc x -> y = x ∨ x < y → ⊥ osucc {ox} {oy} oy<ox with trio< (osuc oy) ox osucc {ox} {oy} oy<ox | tri< a ¬b ¬c = ordtrans a <-osuc osucc {ox} {oy} oy<ox | tri≈ ¬a refl ¬c = <-osuc @@ -57,6 +54,11 @@ osucprev {ox} {oy} oy<ox | tri≈ ¬a b ¬c = ⊥-elim (o<¬≡ (cong (λ k → osuc k) b) oy<ox ) osucprev {ox} {oy} oy<ox | tri> ¬a ¬b c = ⊥-elim (o<> (osucc c) oy<ox ) +ordtrans≤-< : {ox oy oz : Ordinal } → ox o< osuc oy → oy o< oz → ox o< oz +ordtrans≤-< {ox} {oy} {oz} x≤y y<z with osuc-≡< x≤y +... | case1 x=y = subst ( λ k → k o< oz ) (sym x=y) y<z +... | case2 x<y = ordtrans x<y y<z + open _∧_ osuc2 : ( x y : Ordinal ) → ( osuc x o< osuc (osuc y )) ⇔ (x o< osuc y) @@ -74,6 +76,12 @@ _o≤_ : Ordinal → Ordinal → Set n a o≤ b = a o< osuc b -- (a ≡ b) ∨ ( a o< b ) +o<→≤ : {a b : Ordinal} → a o< b → a o≤ b +o<→≤ {a} {b} lt with trio< a (osuc b) +... | tri< a₁ ¬b ¬c = a₁ +... | tri≈ ¬a b₁ ¬c = ⊥-elim (¬a (ordtrans lt <-osuc ) ) +... | tri> ¬a ¬b c = ⊥-elim (¬a (ordtrans lt <-osuc ) ) + -- o<-irr : { x y : Ordinal } → { lt lt1 : x o< y } → lt ≡ lt1 xo<ab : {oa ob : Ordinal } → ( {ox : Ordinal } → ox o< oa → ox o< ob ) → oa o< osuc ob
--- a/src/ordinal.agda Sat Jun 25 17:36:18 2022 +0900 +++ b/src/ordinal.agda Thu Jun 30 06:57:05 2022 +0900 @@ -1,13 +1,13 @@ -open import Level +open import Level module ordinal where open import logic open import nat -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 _n⊔_ ) open import Data.Empty open import Relation.Binary.PropositionalEquality open import Relation.Binary.Definitions -open import Data.Nat.Properties +open import Data.Nat.Properties as NP open import Relation.Nullary open import Relation.Binary.Core @@ -16,30 +16,30 @@ -- Countable Ordinals -- -data OrdinalD {n : Level} : (lv : Nat) → Set n where - Φ : (lv : Nat) → OrdinalD lv - OSuc : (lv : Nat) → OrdinalD {n} lv → OrdinalD lv +data OrdinalD {n : Level} : (lv : ℕ) → Set n where + Φ : (lv : ℕ) → OrdinalD lv + OSuc : (lv : ℕ) → OrdinalD {n} lv → OrdinalD lv record Ordinal {n : Level} : Set n where constructor ordinal field - lv : Nat + lv : ℕ ord : OrdinalD {n} lv -data _d<_ {n : Level} : {lx ly : Nat} → OrdinalD {n} lx → OrdinalD {n} ly → Set n where - Φ< : {lx : Nat} → {x : OrdinalD {n} lx} → Φ lx d< OSuc lx x - s< : {lx : Nat} → {x y : OrdinalD {n} lx} → x d< y → OSuc lx x d< OSuc lx y +data _d<_ {n : Level} : {lx ly : ℕ} → OrdinalD {n} lx → OrdinalD {n} ly → Set n where + Φ< : {lx : ℕ} → {x : OrdinalD {n} lx} → Φ lx d< OSuc lx x + s< : {lx : ℕ} → {x y : OrdinalD {n} lx} → x d< y → OSuc lx x d< OSuc lx y open Ordinal _o<_ : {n : Level} ( x y : Ordinal ) → Set n _o<_ x y = (lv x < lv y ) ∨ ( ord x d< ord y ) -s<refl : {n : Level } {lx : Nat } { x : OrdinalD {n} lx } → x d< OSuc lx x +s<refl : {n : Level } {lx : ℕ } { x : OrdinalD {n} lx } → x d< OSuc lx x s<refl {n} {lv} {Φ lv} = Φ< s<refl {n} {lv} {OSuc lv x} = s< s<refl -trio<> : {n : Level} → {lx : Nat} {x : OrdinalD {n} lx } { y : OrdinalD lx } → y d< x → x d< y → ⊥ +trio<> : {n : Level} → {lx : ℕ} {x : OrdinalD {n} lx } { y : OrdinalD lx } → y d< x → x d< y → ⊥ trio<> {n} {lx} {.(OSuc lx _)} {.(OSuc lx _)} (s< s) (s< t) = trio<> s t trio<> {n} {lx} {.(OSuc lx _)} {.(Φ lx)} Φ< () @@ -56,16 +56,16 @@ lv x ≡ lv y → ord x ≅ ord y → x ≡ y ordinal-cong refl refl = refl -≡→¬d< : {n : Level} → {lv : Nat} → {x : OrdinalD {n} lv } → x d< x → ⊥ +≡→¬d< : {n : Level} → {lv : ℕ} → {x : OrdinalD {n} lv } → x d< x → ⊥ ≡→¬d< {n} {lx} {OSuc lx y} (s< t) = ≡→¬d< t -trio<≡ : {n : Level} → {lx : Nat} {x : OrdinalD {n} lx } { y : OrdinalD lx } → x ≡ y → x d< y → ⊥ +trio<≡ : {n : Level} → {lx : ℕ} {x : OrdinalD {n} lx } { y : OrdinalD lx } → x ≡ y → x d< y → ⊥ trio<≡ refl = ≡→¬d< -trio>≡ : {n : Level} → {lx : Nat} {x : OrdinalD {n} lx } { y : OrdinalD lx } → x ≡ y → y d< x → ⊥ +trio>≡ : {n : Level} → {lx : ℕ} {x : OrdinalD {n} lx } { y : OrdinalD lx } → x ≡ y → y d< x → ⊥ trio>≡ refl = ≡→¬d< -triOrdd : {n : Level} → {lx : Nat} → Trichotomous _≡_ ( _d<_ {n} {lx} {lx} ) +triOrdd : {n : Level} → {lx : ℕ} → Trichotomous _≡_ ( _d<_ {n} {lx} {lx} ) triOrdd {_} {lv} (Φ lv) (Φ lv) = tri≈ ≡→¬d< refl ≡→¬d< triOrdd {_} {lv} (Φ lv) (OSuc lv y) = tri< Φ< (λ ()) ( λ lt → trio<> lt Φ< ) triOrdd {_} {lv} (OSuc lv x) (Φ lv) = tri> (λ lt → trio<> lt Φ<) (λ ()) Φ< @@ -97,7 +97,7 @@ o<> {n} {record { lv = lv₁ ; ord = .(OSuc lv₁ _) }} {record { lv = .lv₁ ; ord = .(OSuc lv₁ _) }} (case2 (s< y<x)) (case2 (s< x<y)) = o<> (case2 y<x) (case2 x<y) -orddtrans : {n : Level} {lx : Nat} {x y z : OrdinalD {n} lx } → x d< y → y d< z → x d< z +orddtrans : {n : Level} {lx : ℕ} {x y z : OrdinalD {n} lx } → x d< y → y d< z → x d< z orddtrans {_} {lx} {.(Φ lx)} {.(OSuc lx _)} {.(OSuc lx _)} Φ< (s< y<z) = Φ< orddtrans {_} {lx} {.(OSuc lx _)} {.(OSuc lx _)} {.(OSuc lx _)} (s< x<y) (s< y<z) = s< ( orddtrans x<y y<z ) @@ -163,11 +163,11 @@ open _∧_ TransFinite : {n m : Level} → { ψ : Ordinal {suc n} → Set m } - → ( ∀ (lx : Nat ) → ( (x : Ordinal {suc n} ) → x o< ordinal lx (Φ lx) → ψ x ) → ψ ( record { lv = lx ; ord = Φ lx } ) ) - → ( ∀ (lx : Nat ) → (x : OrdinalD lx ) → ( (y : Ordinal {suc n} ) → y o< ordinal lx (OSuc lx x) → ψ y ) → ψ ( record { lv = lx ; ord = OSuc lx x } ) ) + → ( ∀ (lx : ℕ ) → ( (x : Ordinal {suc n} ) → x o< ordinal lx (Φ lx) → ψ x ) → ψ ( record { lv = lx ; ord = Φ lx } ) ) + → ( ∀ (lx : ℕ ) → (x : OrdinalD lx ) → ( (y : Ordinal {suc n} ) → y o< ordinal lx (OSuc lx x) → ψ y ) → ψ ( record { lv = lx ; ord = OSuc lx x } ) ) → ∀ (x : Ordinal) → ψ x TransFinite {n} {m} {ψ} caseΦ caseOSuc x = proj1 (TransFinite1 (lv x) (ord x) ) where - TransFinite1 : (lx : Nat) (ox : OrdinalD lx ) → ψ (ordinal lx ox) ∧ ( ( (x : Ordinal {suc n} ) → x o< ordinal lx ox → ψ x ) ) + TransFinite1 : (lx : ℕ) (ox : OrdinalD lx ) → ψ (ordinal lx ox) ∧ ( ( (x : Ordinal {suc n} ) → x o< ordinal lx ox → ψ x ) ) TransFinite1 Zero (Φ 0) = ⟪ caseΦ Zero lemma , lemma1 ⟫ where lemma : (x : Ordinal) → x o< ordinal Zero (Φ Zero) → ψ x lemma x (case1 ()) @@ -176,9 +176,9 @@ lemma1 x (case1 ()) lemma1 x (case2 ()) TransFinite1 (Suc lx) (Φ (Suc lx)) = ⟪ caseΦ (Suc lx) (λ x → lemma (lv x) (ord x)) , (λ x → lemma (lv x) (ord x)) ⟫ where - lemma0 : (ly : Nat) (oy : OrdinalD ly ) → ordinal ly oy o< ordinal lx (Φ lx) → ψ (ordinal ly oy) + lemma0 : (ly : ℕ) (oy : OrdinalD ly ) → ordinal ly oy o< ordinal lx (Φ lx) → ψ (ordinal ly oy) lemma0 ly oy lt = proj2 ( TransFinite1 lx (Φ lx) ) (ordinal ly oy) lt - lemma : (ly : Nat) (oy : OrdinalD ly ) → ordinal ly oy o< ordinal (Suc lx) (Φ (Suc lx)) → ψ (ordinal ly oy) + lemma : (ly : ℕ) (oy : OrdinalD ly ) → ordinal ly oy o< ordinal (Suc lx) (Φ (Suc lx)) → ψ (ordinal ly oy) lemma lx1 ox1 (case1 lt) with <-∨ lt lemma lx (Φ lx) (case1 lt) | case1 refl = proj1 ( TransFinite1 lx (Φ lx) ) lemma lx (Φ lx) (case1 lt) | case2 lt1 = lemma0 lx (Φ lx) (case1 lt1) @@ -200,17 +200,34 @@ lemma y lt | case1 refl = proj1 ( TransFinite1 lx ox ) lemma y lt | case2 lt1 = proj2 ( TransFinite1 lx ox ) y lt1 -open import Data.Nat.Properties as DP OrdIrr : {n : Level } {x y : Ordinal {suc n} } {lt lt1 : x o< y} → lt ≡ lt1 -OrdIrr {n} {ordinal lv₁ ord₁} {ordinal lv₂ ord₂} {case1 x} {case1 x₁} = cong case1 (DP.<-irrelevant _ _ ) +OrdIrr {n} {ordinal lv₁ ord₁} {ordinal lv₂ ord₂} {case1 x} {case1 x₁} = cong case1 (NP.<-irrelevant _ _ ) OrdIrr {n} {ordinal lv₁ ord₁} {ordinal lv₂ ord₂} {case1 x} {case2 x₁} = ⊥-elim ( nat-≡< ( d<→lv x₁ ) x ) OrdIrr {n} {ordinal lv₁ ord₁} {ordinal lv₂ ord₂} {case2 x} {case1 x₁} = ⊥-elim ( nat-≡< ( d<→lv x ) x₁ ) OrdIrr {n} {ordinal lv₁ .(Φ lv₁)} {ordinal .lv₁ .(OSuc lv₁ _)} {case2 Φ<} {case2 Φ<} = refl OrdIrr {n} {ordinal lv₁ (OSuc lv₁ a)} {ordinal .lv₁ (OSuc lv₁ b)} {case2 (s< x)} {case2 (s< x₁)} = cong (λ k → case2 (s< k)) (lemma1 _ _ x x₁) where - lemma1 : {lx : Nat} (a b : OrdinalD {suc n} lx) → (x y : a d< b ) → x ≡ y + lemma1 : {lx : ℕ} (a b : OrdinalD {suc n} lx) → (x y : a d< b ) → x ≡ y lemma1 {lx} .(Φ lx) .(OSuc lx _) Φ< Φ< = refl lemma1 {lx} (OSuc lx a) (OSuc lx b) (s< x) (s< y) = cong s< (lemma1 {lx} a b x y ) + +TransFinite3 : {n m : Level} { ψ : Ordinal {suc n} → Set m } + → ( (x : Ordinal {suc n}) → ( (y : Ordinal {suc n} ) → y o< x → ψ y ) → ψ x ) + → ∀ (x : Ordinal {suc n} ) → ψ x +TransFinite3 {n} {m} {ψ} ind x = TransFinite {n} {m} {ψ} caseΦ caseOSuc x where + caseΦ : (lx : ℕ) → ((x₁ : Ordinal {suc n}) → x₁ o< ordinal lx (Φ lx) → ψ x₁) → + ψ (record { lv = lx ; ord = Φ lx }) + caseΦ lx prev = ind (ordinal lx (Φ lx) ) prev + caseOSuc : (lx : ℕ) (x₁ : OrdinalD lx) → ((y : Ordinal) → y o< ordinal lx (OSuc lx x₁) → ψ y) → + ψ (record { lv = lx ; ord = OSuc lx x₁ }) + caseOSuc lx ox prev = ind (ordinal lx (OSuc lx ox)) prev + +-- TP : {n m l : Level} → {Q : Ordinal {suc n} → Set m} {P : { x y : Ordinal {suc n} } → Q x → Q y → Set l} +-- → ( ind : (x : Ordinal {suc n}) → ( (y : Ordinal {suc n} ) → y o< x → Q y ) → Q x ) +-- → ( (x : Ordinal {suc n} ) → ( prev : (y : Ordinal {suc n} ) → y o< x → Q y ) → {y : Ordinal {suc n}} → (y<x : y o< x) → P (prev y y<x) (ind x prev) ) +-- → {x z : Ordinal {suc n} } → (z≤x : z o< osuc x ) → P (TransFinite3 {n} {m} { λ x → Q x } {!!} x ) {!!} -- P (TransFinite {?} ind z) (TransFinite {?} ind x ) +-- TP = ? + open import Ordinals C-Ordinal : {n : Level} → Ordinals {suc n} @@ -250,7 +267,7 @@ lemma2 (ordinal Zero (OSuc 0 dx)) (case2 (s< x)) (case1 (s≤s z≤n)) not = not _ refl lemma2 (ordinal (Suc lx) (OSuc (Suc lx) ox)) y<x (case1 (s≤s (s≤s lt))) not = not _ refl lemma2 (ordinal (Suc lx) (Φ (Suc lx))) (case1 x) (case1 (s≤s (s≤s lt))) not = lemma3 x lt where - lemma3 : {n l : Nat} → (Suc (Suc n) ≤ Suc l) → l ≤ n → ⊥ + lemma3 : {n l : ℕ} → (Suc (Suc n) ≤ Suc l) → l ≤ n → ⊥ lemma3 (s≤s sn≤l) (s≤s l≤n) = lemma3 sn≤l l≤n open Oprev Oprev-p : (x : Ordinal) → Dec ( Oprev (Ordinal {suc n}) osuc x ) @@ -263,13 +280,13 @@ TransFinite2 : { ψ : ord1 → Set (suc (suc n)) } → ( (x : ord1) → ( (y : ord1 ) → y o< x → ψ y ) → ψ x ) → ∀ (x : ord1) → ψ x - TransFinite2 {ψ} lt x = TransFinite {n} {suc (suc n)} {ψ} caseΦ caseOSuc x where - caseΦ : (lx : Nat) → ((x₁ : Ordinal) → x₁ o< ordinal lx (Φ lx) → ψ x₁) → + TransFinite2 {ψ} ind x = TransFinite {n} {suc (suc n)} {ψ} caseΦ caseOSuc x where + caseΦ : (lx : ℕ) → ((x₁ : Ordinal) → x₁ o< ordinal lx (Φ lx) → ψ x₁) → ψ (record { lv = lx ; ord = Φ lx }) - caseΦ lx prev = lt (ordinal lx (Φ lx) ) prev - caseOSuc : (lx : Nat) (x₁ : OrdinalD lx) → ((y : Ordinal) → y o< ordinal lx (OSuc lx x₁) → ψ y) → + caseΦ lx prev = ind (ordinal lx (Φ lx) ) prev + caseOSuc : (lx : ℕ) (x₁ : OrdinalD lx) → ((y : Ordinal) → y o< ordinal lx (OSuc lx x₁) → ψ y) → ψ (record { lv = lx ; ord = OSuc lx x₁ }) - caseOSuc lx ox prev = lt (ordinal lx (OSuc lx ox)) prev + caseOSuc lx ox prev = ind (ordinal lx (OSuc lx ox)) prev -- H-Ordinal : {n : Level} → Ordinals {suc n} → Ordinals {suc n} → Ordinals {suc n}
--- a/src/zorn.agda Sat Jun 25 17:36:18 2022 +0900 +++ b/src/zorn.agda Thu Jun 30 06:57:05 2022 +0900 @@ -230,23 +230,37 @@ x=fy : x ≡ f y record IsSup (A B : HOD) {x : Ordinal } (xa : odef A x) : Set n where - field + ield x<sup : {y : Ordinal} → odef B y → (y ≡ x ) ∨ (y << x ) -record ZChain ( A : HOD ) (x : Ordinal) ( f : Ordinal → Ordinal ) ( z : Ordinal ) : Set (Level.suc n) where +record ZChain1 ( z : Ordinal ) : Set (Level.suc n) where field supf : Ordinal → HOD + chain-mono : {x : Ordinal} → x o≤ z → supf x ⊆' supf z + +ZChain0 : (A : HOD ) → Set (Level.suc n) +ZChain0 A = ZChain1 ( & A ) + +record ZChain ( A : HOD ) (init : Ordinal) ( f : Ordinal → Ordinal ) (zc0 : ZChain0 A ) ( z : Ordinal ) : Set (Level.suc n) where chain : HOD - chain = supf z + chain = ZChain1.supf zc0 z field chain⊆A : chain ⊆' A - chain∋x : odef chain x - initial : {y : Ordinal } → odef chain y → * x ≤ * y + chain∋init : odef chain init + initial : {y : Ordinal } → odef chain y → * init ≤ * y f-next : {a : Ordinal } → odef chain a → odef chain (f a) + f-total : {x : Ordinal} → IsTotalOrderSet chain is-max : {a b : Ordinal } → (ca : odef chain a ) → b o< osuc z → (ab : odef A b) → HasPrev A chain ab f ∨ IsSup A chain ab → * a < * b → odef chain b - pmono : (x : Ordinal ) → x o≤ z → supf x ⊆' supf z + +record UZFChain ( A : HOD ) ( f : Ordinal → Ordinal ) (zc0 : ZChain0 A ) (x y : Ordinal) + (prev : (z : Ordinal) → z o< x → ZChain A y f zc0 z) (z : Ordinal) : Set n where + -- Union of ZFChain from y which has maximality o< x + field + u : Ordinal + u<x : u o< x + chain∋z : odef (ZChain.chain (prev u u<x )) z record Maximal ( A : HOD ) : Set (Level.suc n) where field @@ -319,20 +333,21 @@ cf-is-≤-monotonic : (nmx : ¬ Maximal A ) → ≤-monotonic-f A ( cf nmx ) cf-is-≤-monotonic nmx x ax = ⟪ case2 (proj1 ( cf-is-<-monotonic nmx x ax )) , proj2 ( cf-is-<-monotonic nmx x ax ) ⟫ - sp0 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) (zc : ZChain A (& s) f (& A) ) (total : IsTotalOrderSet (ZChain.chain zc) ) → SUP A (ZChain.chain zc) - sp0 f mf zc total = supP (ZChain.chain zc) (ZChain.chain⊆A zc) total + sp0 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) (zc0 : ZChain0 A) (zc : ZChain A (& s) f zc0 (& A) ) + (total : IsTotalOrderSet (ZChain.chain zc) ) → SUP A (ZChain.chain zc) + sp0 f mf zc0 zc total = supP (ZChain.chain zc) (ZChain.chain⊆A zc) total zc< : {x y z : Ordinal} → {P : Set n} → (x o< y → P) → x o< z → z o< y → P zc< {x} {y} {z} {P} prev x<z z<y = prev (ordtrans x<z z<y) --- --- the maximum chain has fix point of any ≤-monotonic function --- - fixpoint : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) (zc : ZChain A (& s) f (& A) ) + fixpoint : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) (zc0 : ZChain0 A ) (zc : ZChain A (& s) f zc0 (& A) ) → (total : IsTotalOrderSet (ZChain.chain zc) ) - → f (& (SUP.sup (sp0 f mf zc total ))) ≡ & (SUP.sup (sp0 f mf zc total)) - fixpoint f mf zc total = z14 where + → f (& (SUP.sup (sp0 f mf zc0 zc total ))) ≡ & (SUP.sup (sp0 f mf zc0 zc total)) + fixpoint f mf zc0 zc total = z14 where chain = ZChain.chain zc - sp1 = sp0 f mf zc total + sp1 = sp0 f mf zc0 zc total z10 : {a b : Ordinal } → (ca : odef chain a ) → b o< osuc (& A) → (ab : odef A b ) → HasPrev A chain ab f ∨ IsSup A chain {b} ab -- (supO chain (ZChain.chain⊆A zc) (ZChain.f-total zc) ≡ b ) → * a < * b → odef chain b @@ -341,11 +356,11 @@ z11 = c<→o< ( SUP.A∋maximal sp1) z12 : odef chain (& (SUP.sup sp1)) z12 with o≡? (& s) (& (SUP.sup sp1)) - ... | yes eq = subst (λ k → odef chain k) eq ( ZChain.chain∋x zc ) - ... | no ne = z10 {& s} {& (SUP.sup sp1)} ( ZChain.chain∋x zc ) (ordtrans z11 <-osuc ) (SUP.A∋maximal sp1) + ... | yes eq = subst (λ k → odef chain k) eq ( ZChain.chain∋init zc ) + ... | no ne = z10 {& s} {& (SUP.sup sp1)} ( ZChain.chain∋init zc ) (ordtrans z11 <-osuc ) (SUP.A∋maximal sp1) (case2 z19 ) z13 where z13 : * (& s) < * (& (SUP.sup sp1)) - z13 with SUP.x<sup sp1 ( ZChain.chain∋x zc ) + z13 with SUP.x<sup sp1 ( ZChain.chain∋init zc ) ... | case1 eq = ⊥-elim ( ne (cong (&) eq) ) ... | case2 lt = subst₂ (λ j k → j < k ) (sym *iso) (sym *iso) lt z19 : IsSup A chain {& (SUP.sup sp1)} (SUP.A∋maximal sp1) @@ -355,7 +370,7 @@ ... | case1 y=p = case1 (subst (λ k → k ≡ _ ) &iso ( cong (&) y=p )) ... | case2 y<p = case2 (subst (λ k → * y < k ) (sym *iso) y<p ) -- λ {y} zy → subst (λ k → (y ≡ & k ) ∨ (y << & k)) ? (SUP.x<sup sp1 ? ) } - z14 : f (& (SUP.sup (sp0 f mf zc total ))) ≡ & (SUP.sup (sp0 f mf zc total )) + z14 : f (& (SUP.sup (sp0 f mf zc0 zc total ))) ≡ & (SUP.sup (sp0 f mf zc0 zc total )) z14 with total (subst (λ k → odef chain k) (sym &iso) (ZChain.f-next zc z12 )) z12 ... | tri< a ¬b ¬c = ⊥-elim z16 where z16 : ⊥ @@ -376,92 +391,59 @@ -- ZChain forces fix point on any ≤-monotonic function (fixpoint) -- ¬ Maximal create cf which is a <-monotonic function by axiom of choice. This contradicts fix point of ZChain -- - z04 : (nmx : ¬ Maximal A ) → (zc : ZChain A (& s) (cf nmx) (& A)) → IsTotalOrderSet (ZChain.chain zc) → ⊥ - z04 nmx zc total = <-irr0 {* (cf nmx c)} {* c} (subst (λ k → odef A k ) (sym &iso) (proj1 (is-cf nmx (SUP.A∋maximal sp1 )))) + z04 : (nmx : ¬ Maximal A ) → (zc0 : ZChain0 A) (zc : ZChain A (& s) (cf nmx) zc0 (& A)) → IsTotalOrderSet (ZChain.chain zc) → ⊥ + z04 nmx zc0 zc total = <-irr0 {* (cf nmx c)} {* c} (subst (λ k → odef A k ) (sym &iso) (proj1 (is-cf nmx (SUP.A∋maximal sp1 )))) (subst (λ k → odef A (& k)) (sym *iso) (SUP.A∋maximal sp1) ) - (case1 ( cong (*)( fixpoint (cf nmx) (cf-is-≤-monotonic nmx ) zc total ))) -- x ≡ f x ̄ + (case1 ( cong (*)( fixpoint (cf nmx) (cf-is-≤-monotonic nmx ) zc0 zc total ))) -- x ≡ f x ̄ (proj1 (cf-is-<-monotonic nmx c (SUP.A∋maximal sp1 ))) where -- x < f x sp1 : SUP A (ZChain.chain zc) - sp1 = sp0 (cf nmx) (cf-is-≤-monotonic nmx) zc total + sp1 = sp0 (cf nmx) (cf-is-≤-monotonic nmx) zc0 zc total c = & (SUP.sup sp1) -- -- create all ZChains under o< x -- - ys : {y : Ordinal} → (ay : odef A y) (f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → HOD - ys {y} ay f mf = record { od = record { def = λ x → FClosure A f y x } ; odmax = & A ; <odmax = {!!} } - init-chain : {y x : Ordinal} → (ay : odef A y) (f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → x o< osuc y → ZChain A y f x - init-chain {y} {x} ay f mf x≤y = record { chain⊆A = λ fx → A∋fc y f mf fx - ; f-next = λ {x} sx → fsuc x sx ; supf = λ _ → ys ay f mf - ; initial = {!!} ; chain∋x = init ay ; is-max = is-max ; pmono = {!!} } where - i-total : IsTotalOrderSet (ys ay f mf ) - i-total fa fb = subst₂ (λ a b → Tri (a < b) (a ≡ b) (b < a ) ) *iso *iso (fcn-cmp y f mf fa fb) - is-max : {a b : Ordinal} → odef (ys ay f mf) a → - b o< osuc x → (ab : odef A b) → HasPrev A (ys ay f mf) ab f ∨ IsSup A (ys ay f mf) ab → - * a < * b → odef (ys ay f mf) b - is-max {a} {b} yca b≤x ab P a<b = {!!} - initial : {i : Ordinal} → odef (ys ay f mf) i → * y ≤ * i - initial {i} (init ai) = case1 refl - initial .{f x} (fsuc x lt) = {!!} - - record ZChain0 ( A : HOD ) : Set (Level.suc n) where - field - chain : HOD - chain⊆A : chain ⊆' A - sind : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y) → (x : Ordinal) - → ((z : Ordinal) → z o< x → ZChain0 A ) → ZChain0 A + → ((z : Ordinal) → z o< x → ZChain1 z ) → ZChain1 x sind f mf {y} ay x prev with Oprev-p x ... | yes op = sc4 where px = Oprev.oprev op - sc : ZChain0 A + sc : ZChain1 px sc = prev px (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc ) - sc4 : ZChain0 A + sc4 : ZChain1 x sc4 with ODC.∋-p O A (* x) - ... | no noax = sc - ... | yes ax with ODC.p∨¬p O ( HasPrev A (ZChain0.chain sc) ax f ) - ... | case1 pr = sc - ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A (ZChain0.chain sc) ax ) - ... | case1 is-sup = record { chain = schain ; chain⊆A = {!!} } where + ... | no noax = ? + ... | yes ax with ODC.p∨¬p O ( HasPrev A (ZChain1.supf sc x) ax f ) + ... | case1 pr = ? + ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A (ZChain1.supf sc x) ax ) + ... | case1 is-sup = ? where -- A∋sc -- x is a sup of zc - sup0 : SUP A (ZChain0.chain sc ) + sup0 : SUP A (ZChain1.supf sc x ) sup0 = record { sup = * x ; A∋maximal = ax ; x<sup = x21 } where - x21 : {y : HOD} → (ZChain0.chain sc) ∋ y → (y ≡ * x) ∨ (y < * x) + x21 : {y : HOD} → (ZChain1.supf sc x) ∋ y → (y ≡ * x) ∨ (y < * x) x21 {y} zy with IsSup.x<sup is-sup zy ... | case1 y=x = case1 (subst₂ (λ j k → j ≡ * k ) *iso &iso ( cong (*) y=x) ) ... | case2 y<x = case2 (subst₂ (λ j k → j < * k ) *iso &iso y<x ) sp : HOD sp = SUP.sup sup0 schain : HOD - schain = record { od = record { def = λ x → odef (ZChain0.chain sc) x ∨ (FClosure A f (& sp) x) } ; odmax = & A ; <odmax = λ {y} sy → {!!} } - ... | case2 ¬x=sup = sc - ... | no ¬ox with trio< x y - ... | tri< a ¬b ¬c = record { chain = record { od = record { def = λ x → FClosure A f y x } ; odmax = & A ; <odmax = λ {y} sy → {!!}} ; chain⊆A = {!!} } - ... | tri≈ ¬a b ¬c = record { chain = record { od = record { def = λ x → FClosure A f y x } ; odmax = & A ; <odmax = λ {y} sy → {!!}} ; chain⊆A = {!!} } - ... | tri> ¬a ¬b y<x = record { chain = Uz ; chain⊆A = {!!} } where - record Usup (z : Ordinal) : Set n where -- Union of supf from y which has maximality o< x - field - u : Ordinal - u<x : u o< x - chain∋z : odef (ZChain0.chain (prev u u<x )) z - Uz : HOD - Uz = record { od = record { def = λ y → Usup y } ; odmax = & A - ; <odmax = {!!} } -- λ lt → subst (λ k → k o< & A ) &iso (c<→o< (subst (λ k → odef A k ) (sym &iso) (Uz⊆A lt))) } + schain = record { od = record { def = λ x → odef (ZChain1.supf sc x) x ∨ (FClosure A f (& sp) x) } ; odmax = & A ; <odmax = λ {y} sy → {!!} } + ... | case2 ¬x=sup = ? + ... | no ¬ox = ? - - ind : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y) → (x : Ordinal) - → ((z : Ordinal) → z o< x → ZChain A y f z) → ZChain A y f x - ind f mf {y} ay x prev with Oprev-p x + ind : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y) → (zc0 : ZChain0 A) → (x : Ordinal) + → ((z : Ordinal) → z o< x → ZChain A y f zc0 z) → ZChain A y f zc0 x + ind f mf {y} ay zc0 x prev with Oprev-p x ... | yes op = zc4 where -- -- we have previous ordinal to use induction -- px = Oprev.oprev op supf : Ordinal → HOD - supf = ZChain.supf (prev px (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc ) ) - zc : ZChain A y f (Oprev.oprev op) + supf = ZChain1.supf zc0 + zc : ZChain A y f zc0 (Oprev.oprev op) zc = prev px (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc ) zc-b<x : (b : Ordinal ) → b o< x → b o< osuc px zc-b<x b lt = subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) lt @@ -472,13 +454,13 @@ -- no-extenion : ( {a b : Ordinal} → odef (ZChain.chain zc) a → b o< osuc x → (ab : odef A b) → HasPrev A (ZChain.chain zc) ab f ∨ IsSup A (ZChain.chain zc) ab → - * a < * b → odef (ZChain.chain zc) b ) → ZChain A y f x - no-extenion is-max = record { supf = supf0 ; chain⊆A = subst (λ k → k ⊆' A ) seq (ZChain.chain⊆A zc) - ; initial = subst (λ k → {y₁ : Ordinal} → odef k y₁ → * y ≤ * y₁ ) seq (ZChain.initial zc) - ; f-next = subst (λ k → {a : Ordinal} → odef k a → odef k (f a) ) seq (ZChain.f-next zc) - ; chain∋x = subst (λ k → odef k y ) seq (ZChain.chain∋x zc) ; pmono = {!!} + * a < * b → odef (ZChain.chain zc) b ) → ZChain A y f zc0 x + no-extenion is-max = record { supf = supf0 ; chain⊆A = subst (λ k → k ⊆' A ) ? (ZChain.chain⊆A zc) + ; initial = subst (λ k → {y₁ : Ordinal} → odef k y₁ → * y ≤ * y₁ ) ? (ZChain.initial zc) + ; f-next = subst (λ k → {a : Ordinal} → odef k a → odef k (f a) ) ? (ZChain.f-next zc) + ; chain∋init = subst (λ k → odef k y ) ? (ZChain.chain∋init zc) ; pmono = {!!} ; is-max = subst (λ k → {a b : Ordinal} → odef k a → b o< osuc x → (ab : odef A b) → - HasPrev A k ab f ∨ IsSup A k ab → * a < * b → odef k b ) seq is-max } where + HasPrev A k ab f ∨ IsSup A k ab → * a < * b → odef k b ) ? is-max } where supf0 : Ordinal → HOD supf0 z with trio< z x ... | tri< a ¬b ¬c = supf z @@ -495,7 +477,7 @@ ... | tri≈ ¬a b₁ ¬c = ⊥-elim (¬a b<x ) ... | tri> ¬a ¬b c = ⊥-elim (¬a b<x ) - zc4 : ZChain A y f x + zc4 : ZChain A y f zc0 x zc4 with ODC.∋-p O A (* x) ... | no noax = no-extenion zc1 where -- ¬ A ∋ p, just skip zc1 : {a b : Ordinal} → odef (ZChain.chain zc) a → b o< osuc x → (ab : odef A b) → @@ -504,7 +486,7 @@ zc1 {a} {b} za b<ox ab P a<b with osuc-≡< b<ox ... | case1 eq = ⊥-elim ( noax (subst (λ k → odef A k) (trans eq (sym &iso)) ab ) ) ... | case2 lt = ZChain.is-max zc za (zc-b<x b lt) ab P a<b - ... | yes ax with ODC.p∨¬p O ( HasPrev A (ZChain.chain zc) ax f ) -- we have to check adding x preserve is-max ZChain A y f mf supO x + ... | yes ax with ODC.p∨¬p O ( HasPrev A (ZChain.chain zc) ax f ) -- we have to check adding x preserve is-max ZChain A y f mf zc0 x ... | case1 pr = no-extenion zc7 where -- we have previous A ∋ z < x , f z ≡ x, so chain ∋ f z ≡ x because of f-next chain0 = ZChain.chain zc zc7 : {a b : Ordinal} → odef (ZChain.chain zc) a → b o< osuc x → (ab : odef A b) → @@ -516,7 +498,7 @@ ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A (ZChain.chain zc) ax ) ... | case1 is-sup = -- x is a sup of zc record { chain⊆A = {!!} ; f-next = {!!} ; pmono = {!!} - ; initial = {!!} ; chain∋x = {!!} ; is-max = {!!} ; supf = supf0 } where + ; initial = {!!} ; chain∋init = {!!} ; is-max = {!!} ; supf = supf0 } where sup0 : SUP A (ZChain.chain zc) sup0 = record { sup = * x ; A∋maximal = ax ; x<sup = x21 } where x21 : {y : HOD} → ZChain.chain zc ∋ y → (y ≡ * x) ∨ (y < * x) @@ -571,7 +553,7 @@ scnext {x} (case2 sx) = case2 ( fsuc x sx ) scinit : {x : Ordinal} → odef schain x → * y ≤ * x scinit {x} (case1 zx) = ZChain.initial zc zx - scinit {x} (case2 sx) with (s≤fc (& sp) f mf sx ) | SUP.x<sup sup0 (subst (λ k → odef chain0 k ) (sym &iso) ( ZChain.chain∋x zc ) ) + scinit {x} (case2 sx) with (s≤fc (& sp) f mf sx ) | SUP.x<sup sup0 (subst (λ k → odef chain0 k ) (sym &iso) ( ZChain.chain∋init zc ) ) ... | case1 sp=x | case1 y=sp = case1 (trans y=sp (subst (λ k → k ≡ * x ) *iso sp=x ) ) ... | case1 sp=x | case2 y<sp = case2 (subst (λ k → * y < k ) (trans (sym *iso) sp=x) y<sp ) ... | case2 sp<x | case1 y=sp = case2 (subst (λ k → k < * x ) (trans *iso (sym y=sp )) sp<x ) @@ -600,9 +582,9 @@ z24 : IsSup A schain ab → IsSup A (ZChain.chain zc) ab z24 p = record { x<sup = λ {y} zy → IsSup.x<sup p (case1 zy ) } z23 : odef chain0 b - z23 with IsSup.x<sup (z24 p) ( ZChain.chain∋x zc ) - ... | case1 y=b = subst (λ k → odef chain0 k ) y=b ( ZChain.chain∋x zc ) - ... | case2 y<b = ZChain.is-max zc (ZChain.chain∋x zc ) (zc-b<x b b<x) ab (case2 (z24 p)) y<b + z23 with IsSup.x<sup (z24 p) ( ZChain.chain∋init zc ) + ... | case1 y=b = subst (λ k → odef chain0 k ) y=b ( ZChain.chain∋init zc ) + ... | case2 y<b = ZChain.is-max zc (ZChain.chain∋init zc ) (zc-b<x b b<x) ab (case2 (z24 p)) y<b seq : schain ≡ supf0 x seq with trio< x x ... | tri< a ¬b ¬c = ⊥-elim ( ¬b refl ) @@ -624,32 +606,30 @@ ... | case1 pr = ⊥-elim ( ¬fy<x record {y = HasPrev.y pr ; ay = HasPrev.ay pr ; x=fy = trans (trans &iso (sym b=x) ) (HasPrev.x=fy pr ) } ) ... | case2 b=sup = ⊥-elim ( ¬x=sup record { x<sup = λ {y} zy → subst (λ k → (y ≡ k) ∨ (y << k)) (trans b=x (sym &iso)) (IsSup.x<sup b=sup zy) } ) - ... | no ¬ox with trio< x y - ... | tri< a ¬b ¬c = init-chain ay f mf {!!} - ... | tri≈ ¬a b ¬c = init-chain ay f mf {!!} - ... | tri> ¬a ¬b y<x = record { supf = supf0 ; chain⊆A = {!!} ; f-next = {!!} ; pmono = {!!} - ; initial = {!!} ; chain∋x = {!!} ; is-max = {!!} } where --- limit ordinal case - record UZFChain (z : Ordinal) : Set n where -- Union of ZFChain from y which has maximality o< x - field - u : Ordinal - u<x : u o< x - chain∋z : odef (ZChain.chain (prev u u<x )) z - Uz⊆A : {z : Ordinal} → UZFChain z → odef A z - Uz⊆A {z} u = ZChain.chain⊆A ( prev (UZFChain.u u) (UZFChain.u<x u) ) (UZFChain.chain∋z u) - uzc : {z : Ordinal} → (u : UZFChain z) → ZChain A y f (UZFChain.u u) + ... | no ¬ox = record { chain⊆A = ? ; f-next = ? ; chain = ? + ; initial = ? ; chain∋init = ? ; is-max = {!!} } where --- limit ordinal case + supf : Ordinal → HOD + supf = ZChain1.supf zc0 + Uz⊆A : {z : Ordinal} → UZFChain A f zc0 x y prev z ∨ FClosure A f y z → odef A z + Uz⊆A {z} (case1 u) = ZChain.chain⊆A ( prev (UZFChain.u u) (UZFChain.u<x u) ) (UZFChain.chain∋z u) + Uz⊆A (case2 lt) = A∋fc _ f mf lt + uzc : {z : Ordinal} → (u : UZFChain A f zc0 x y prev z) → ZChain A y f zc0 (UZFChain.u u) uzc {z} u = prev (UZFChain.u u) (UZFChain.u<x u) Uz : HOD - Uz = record { od = record { def = λ y → UZFChain y } ; odmax = & A + Uz = record { od = record { def = λ z → UZFChain A f zc0 x y prev z ∨ FClosure A f y z } ; odmax = & A ; <odmax = λ lt → subst (λ k → k o< & A ) &iso (c<→o< (subst (λ k → odef A k ) (sym &iso) (Uz⊆A lt))) } u-next : {z : Ordinal} → odef Uz z → odef Uz (f z) - u-next {z} u = record { u = UZFChain.u u ; u<x = UZFChain.u<x u ; chain∋z = ZChain.f-next ( uzc u ) (UZFChain.chain∋z u) } + u-next {z} (case1 u) = case1 record { u = UZFChain.u u ; u<x = UZFChain.u<x u ; chain∋z = ZChain.f-next ( uzc u ) (UZFChain.chain∋z u) } + u-next {z} (case2 u) = case2 ( fsuc _ u ) u-initial : {z : Ordinal} → odef Uz z → * y ≤ * z - u-initial {z} u = ZChain.initial ( uzc u ) (UZFChain.chain∋z u) - u-chain∋x : odef Uz y - u-chain∋x = record { u = y ; u<x = y<x ; chain∋z = ZChain.chain∋x (prev y y<x ) } + u-initial {z} (case1 u) = ZChain.initial ( uzc u ) (UZFChain.chain∋z u) + u-initial {z} (case2 u) = s≤fc _ f mf u + u-chain∋init : odef Uz y + u-chain∋init = case2 ( init ay ) + supf0 : Ordinal → HOD supf0 z with trio< z x - ... | tri< a ¬b ¬c = ZChain.supf (prev z a ) z + ... | tri< a ¬b ¬c = ZChain1.supf zc0 z ... | tri≈ ¬a b ¬c = Uz ... | tri> ¬a ¬b c = Uz seq : Uz ≡ supf0 x @@ -657,52 +637,21 @@ ... | tri< a ¬b ¬c = ⊥-elim ( ¬b refl ) ... | tri≈ ¬a b ¬c = refl ... | tri> ¬a ¬b c = refl - seq<x : {b : Ordinal } → (b<x : b o< x ) → ZChain.supf (prev b b<x ) b ≡ supf0 b + seq<x : {b : Ordinal } → (b<x : b o< x ) → ZChain1.supf zc0 b ≡ supf0 b seq<x {b} b<x with trio< b x - ... | tri< a ¬b ¬c = cong (λ k → ZChain.supf (prev b k ) b) o<-irr -- b<x ≡ a + ... | tri< a ¬b ¬c = cong (λ k → ZChain1.supf zc0 b) o<-irr -- b<x ≡ a ... | tri≈ ¬a b₁ ¬c = ⊥-elim (¬a b<x ) ... | tri> ¬a ¬b c = ⊥-elim (¬a b<x ) ord≤< : {x y z : Ordinal} → x o< z → z o≤ y → x o< y ord≤< {x} {y} {z} x<z z≤y with osuc-≡< z≤y ... | case1 z=y = subst (λ k → x o< k ) z=y x<z ... | case2 z<y = ordtrans x<z z<y - u-mono : {z : Ordinal} → z o≤ x → supf0 z ⊆' supf0 x - u-mono {z} z≤x {i} with trio< z x | trio< x x - ... | tri< a ¬b ¬c | tri< a₁ ¬b₁ ¬c₁ = λ lt → {!!} - ... | tri< a ¬b ¬c | tri≈ ¬a b ¬c₁ = λ lt → record { u = {!!} ; u<x = {!!} ; chain∋z = lt } - ... | tri< a ¬b ¬c | tri> ¬a ¬b₁ c = λ lt → {!!} - ... | tri≈ ¬a b ¬c | s = {!!} -- λ lt → lt - ... | tri> ¬a ¬b c | s = {!!} -- λ lt → lt - SZ : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → {y : Ordinal} (ya : odef A y) → ZChain A y f (& A) - SZ f mf {y} ay = TransFinite {λ z → ZChain A y f z } (ind f mf ay ) (& A) - - postulate - TFcomm : { ψ : Ordinal → Set (Level.suc n) } - → (ind : (x : Ordinal) → ( (y : Ordinal ) → y o< x → ψ y ) → ψ x ) - → ∀ (x : Ordinal) → ind x (λ y _ → TransFinite ind y ) ≡ TransFinite ind x + SZ0 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → {y : Ordinal} (ya : odef A y) → ZChain0 A + SZ0 f mf ay = TransFinite {λ z → ZChain1 z} (sind f mf ay ) (& A) - record ZChain1 ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y) : Set (Level.suc n) where - field - zc : ZChain A y f (& A) - supf = ZChain.supf zc - field - chain-mono : {x y : Ordinal} → x o≤ y → supf x ⊆' supf y - f-total : {x : Ordinal} → IsTotalOrderSet (supf x) - - SZ1 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → {y : Ordinal} → (ay : odef A y) - → ZChain1 f mf ay - SZ1 f mf {y} ay = record { zc = TransFinite {λ z → ZChain A y f z } (ind f mf ay ) (& A) - ; chain-mono = mono sf ; f-total = {!!} } where -- TransFinite {λ w → ZChain1 f mf ay w} indp z where - sf : Ordinal → HOD - sf x = ZChain.supf (TransFinite (ind f mf ay) (& A)) x - sf' : Ordinal → HOD - sf' x = ZChain.supf (ind f mf ay (& A) {!!} ) x - mono : {x : Ordinal} {w : Ordinal} (sf : Ordinal → HOD) → x o≤ w → sf x ⊆' sf w - mono {a} {b} sf a≤b = TransFinite0 {λ b → a o≤ b → sf a ⊆' sf b } mind b a≤b where - mind : (x : Ordinal) → ((y₁ : Ordinal) → y₁ o< x → a o≤ y₁ → sf a ⊆' sf y₁) → a o≤ x → sf a ⊆' sf x - mind x prev a≤x sai = {!!} - + SZ : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → {y : Ordinal} (ya : odef A y) → ZChain A y f (SZ0 f mf ya) (& A) + SZ f mf {y} ay = TransFinite {λ z → ZChain A y f (SZ0 f mf ay) z } (ind f mf ay (SZ0 f mf ay) ) (& A) zorn00 : Maximal A zorn00 with is-o∅ ( & HasMaximal ) -- we have no Level (suc n) LEM @@ -714,16 +663,18 @@ zorn01 = proj1 zorn03 zorn02 : {x : HOD} → A ∋ x → ¬ (ODC.minimal O HasMaximal (λ eq → not (=od∅→≡o∅ eq)) < x) zorn02 {x} ax m<x = proj2 zorn03 (& x) ax (subst₂ (λ j k → j < k) (sym *iso) (sym *iso) m<x ) - ... | yes ¬Maximal = ⊥-elim ( z04 nmx zorn04 total ) where + ... | yes ¬Maximal = ⊥-elim ( z04 nmx zc0 zorn04 total ) where -- if we have no maximal, make ZChain, which contradict SUP condition nmx : ¬ Maximal A nmx mx = ∅< {HasMaximal} zc5 ( ≡o∅→=od∅ ¬Maximal ) where zc5 : odef A (& (Maximal.maximal mx)) ∧ (( y : Ordinal ) → odef A y → ¬ (* (& (Maximal.maximal mx)) < * y)) zc5 = ⟪ Maximal.A∋maximal mx , (λ y ay mx<y → Maximal.¬maximal<x mx (subst (λ k → odef A k ) (sym &iso) ay) (subst (λ k → k < * y) *iso mx<y) ) ⟫ - zorn04 : ZChain A (& s) (cf nmx) (& A) - zorn04 = ZChain1.zc ( SZ1 (cf nmx) (cf-is-≤-monotonic nmx) (subst (λ k → odef A k ) &iso as ) ) + zc0 : ZChain0 A + zc0 = TransFinite {λ z → ZChain1 z} (sind (cf nmx) (cf-is-≤-monotonic nmx) (subst (λ k → odef A k ) &iso as )) (& A) + zorn04 : ZChain A (& s) (cf nmx) zc0 (& A) + zorn04 = SZ (cf nmx) (cf-is-≤-monotonic nmx) (subst (λ k → odef A k ) &iso as ) total : IsTotalOrderSet (ZChain.chain zorn04) - total = ZChain1.f-total (SZ1 (cf nmx) (cf-is-≤-monotonic nmx) (subst (λ k → odef A k ) &iso as) ) + total = ZChain.f-total (SZ (cf nmx) (cf-is-≤-monotonic nmx) (subst (λ k → odef A k ) &iso as) ) -- usage (see filter.agda ) --