Members/kono/Proof/ZF-in-agda: src/zorn.agda comparison

comparison src/zorn.agda @ 804:2d84411a636e

...

author	Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date	Thu, 11 Aug 2022 14:07:57 +0900
parents	7c6612b753b9
children	9d97134d0a93

comparison

equal deleted inserted replaced

-:7c6612b753b9
+:2d84411a636e
 x<sup   : {y : Ordinal} → odef B y → (y ≡ x ) ∨ (y << x )
 record SUP ( A B : HOD )  : Set (Level.suc n) where
 field
 sup : HOD
-A∋maximal : A ∋ sup
+as : A ∋ sup
 x<sup : {x : HOD} → B ∋ x → (x ≡ sup ) ∨ (x < sup )   -- B is Total, use positive
 --
 --  sup and its fclosure is in a chain HOD
 --    chain HOD is sorted by sup as Ordinal and <-ordered
 → * a < * b  → odef ((UnionCF A f mf ay (ZChain.supf zc) z)) b
 record Maximal ( A : HOD )  : Set (Level.suc n) where
 field
 maximal : HOD
-A∋maximal : A ∋ maximal
+as : A ∋ maximal
 ¬maximal<x : {x : HOD} → A ∋ x  → ¬ maximal < x       -- A is Partial, use negative
 -- data UChain is total
 chain-total : (A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f)  {y : Ordinal} (ay : odef A y) (supf : Ordinal → Ordinal )
 no-maximum : HasMaximal =h= od∅ → (x : Ordinal) → odef A x ∧ ((m : Ordinal) →  odef A m →  odef A x ∧ (¬ (* x < * m) )) →  ⊥
 no-maximum nomx x P = ¬x<0 (eq→ nomx {x} ⟪ proj1 P , (λ m ma p → proj2 ( proj2 P m ma ) p ) ⟫ )
 Gtx : { x : HOD} → A ∋ x → HOD
 Gtx {x} ax = record { od = record { def = λ y → odef A y ∧ (x < (* y)) } ; odmax = & A ; <odmax = z07 }
 z08  : ¬ Maximal A →  HasMaximal =h= od∅
-z08 nmx  = record { eq→  = λ {x} lt → ⊥-elim ( nmx record {maximal = * x ; A∋maximal = subst (λ k → odef A k) (sym &iso) (proj1 lt)
+z08 nmx  = record { eq→  = λ {x} lt → ⊥-elim ( nmx record {maximal = * x ; as = subst (λ k → odef A k) (sym &iso) (proj1 lt)
 ; ¬maximal<x = λ {y} ay → subst (λ k → ¬ (* x < k)) *iso (proj2 lt (& y) ay) } ) ; eq← =  λ {y} lt → ⊥-elim ( ¬x<0 lt )}
 x-is-maximal : ¬ Maximal A → {x : Ordinal} → (ax : odef A x) → & (Gtx (subst (λ k → odef A k ) (sym &iso) ax)) ≡ o∅ → (m : Ordinal) → odef A m → odef A x ∧ (¬ (* x < * m))
 x-is-maximal nmx {x} ax nogt m am  = ⟪ subst (λ k → odef A k) &iso (subst (λ k → odef A k ) (sym &iso) ax) ,  ¬x<m  ⟫ where
 ¬x<m :  ¬ (* x < * m)
 ¬x<m x<m = ∅< {Gtx (subst (λ k → odef A k ) (sym &iso) ax)} {* m} ⟪ subst (λ k → odef A k) (sym &iso) am , subst (λ k → * x < k ) (cong (*) (sym &iso)) x<m ⟫  (≡o∅→=od∅ nogt)
 z10 :  {a b : Ordinal } → (ca : odef chain a ) → b o< & 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
 z10 = ZChain1.is-max (SZ1 f mf as0 zc (& A) )
 z11 : & (SUP.sup sp1) o< & A
-z11 = c<→o< ( SUP.A∋maximal sp1)
+z11 = c<→o< ( SUP.as sp1)
 z12 : odef chain (& (SUP.sup sp1))
 z12 with o≡? (& s) (& (SUP.sup sp1))
 ... | yes eq = subst (λ k → odef chain k) eq ( ZChain.chain∋init zc )
-... | no ne = z10 {& s} {& (SUP.sup sp1)} ( ZChain.chain∋init zc ) z11 (SUP.A∋maximal sp1)
+... | no ne = z10 {& s} {& (SUP.sup sp1)} ( ZChain.chain∋init zc ) z11 (SUP.as sp1)
 (case2 z19 ) z13 where
 z13 :  * (& s) < * (& (SUP.sup sp1))
 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)
+z19 : IsSup A chain {& (SUP.sup sp1)} (SUP.as sp1)
 z19 = record {   x<sup = z20 }  where
 z20 :  {y : Ordinal} → odef chain y → (y ≡ & (SUP.sup sp1)) ∨ (y << & (SUP.sup sp1))
 z20 {y} zy with SUP.x<sup sp1 (subst (λ k → odef chain k ) (sym &iso) zy)
 ... | 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 with total (subst (λ k → odef chain k) (sym &iso)  (ZChain.f-next zc z12 )) z12
 ... | tri< a ¬b ¬c = ⊥-elim z16 where
 z16 : ⊥
-z16 with proj1 (mf (& ( SUP.sup sp1)) ( SUP.A∋maximal sp1 ))
+z16 with proj1 (mf (& ( SUP.sup sp1)) ( SUP.as sp1 ))
 ... | case1 eq = ⊥-elim (¬b (subst₂ (λ j k → j ≡ k ) refl *iso (sym eq) ))
 ... | case2 lt = ⊥-elim (¬c (subst₂ (λ j k → k < j ) refl *iso lt ))
 ... | tri≈ ¬a b ¬c = subst ( λ k → k ≡ & (SUP.sup sp1) ) &iso ( cong (&) b )
 ... | tri> ¬a ¬b c = ⊥-elim z17 where
 z15 : (* (f ( & ( SUP.sup sp1 ))) ≡ SUP.sup sp1) ∨ (* (f ( & ( SUP.sup sp1 ))) <  SUP.sup sp1)
 -- ¬ 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 (cf nmx) (cf-is-≤-monotonic nmx) as0 (& 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 zc total = <-irr0  {* (cf nmx c)} {* c} (subst (λ k → odef A k ) (sym &iso) (proj1 (is-cf nmx (SUP.as  sp1 ))))
-(subst (λ k → odef A (& k)) (sym *iso) (SUP.A∋maximal sp1) )
+(subst (λ k → odef A (& k)) (sym *iso) (SUP.as sp1) )
 (case1 ( cong (*)( fixpoint (cf nmx) (cf-is-≤-monotonic nmx ) zc total ))) -- x ≡ f x ̄
-(proj1 (cf-is-<-monotonic nmx c (SUP.A∋maximal sp1 ))) where          -- x < f x
+(proj1 (cf-is-<-monotonic nmx c (SUP.as sp1 ))) where          -- x < f x
 sp1 : SUP A (ZChain.chain zc)
 sp1 = sp0 (cf nmx) (cf-is-≤-monotonic nmx) zc total
 c = & (SUP.sup sp1)
 uchain : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y) → HOD
 ysup : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y)
 →  SUP A (uchain f mf ay)
 ysup f mf {y} ay = supP (uchain f mf ay) (λ lt → A∋fc y f mf lt)  (utotal f mf ay)
-initChain : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y) → ZChain A f mf ay o∅
-initChain f mf {y} ay = record { supf = isupf ; chain⊆A = λ lt → proj1 lt ; chain∋init = cy  ; sup = {!!} ; supf-is-sup = {!!}
-; initial = isy ; f-next = inext ; f-total = itotal ; sup=u = λ _ b<0 → ? ; csupf = {!!} } where
-spi =  & (SUP.sup (ysup f mf ay))
-isupf : Ordinal → Ordinal
-isupf z = spi
-sp = ysup f mf ay
-asi = SUP.A∋maximal sp
-cy : odef (UnionCF A f mf ay isupf o∅) y
-cy = ⟪ ay , ch-init (init ay refl)  ⟫
-y<sup : * y ≤ SUP.sup (ysup f mf ay)
-y<sup = SUP.x<sup  (ysup f mf ay) (subst (λ k → FClosure A f y k ) (sym &iso) (init ay refl))
-sup : {x : Ordinal} → x o< o∅ → SUP A (UnionCF A f mf ay isupf x)
-sup {x} lt = ⊥-elim ( ¬x<0 lt )
-isy : {z : Ordinal } → odef (UnionCF A f mf ay isupf o∅) z → * y ≤ * z
-isy {z} ⟪ az , uz ⟫ with uz
-... | ch-init fc = s≤fc y f mf fc
-... | ch-is-sup u u≤x is-sup fc = ≤-ftrans (subst (λ k → * y ≤ k) (sym *iso) y<sup)  (s≤fc (& (SUP.sup (ysup f mf ay))) f mf fc )
-inext : {a : Ordinal} → odef (UnionCF A f mf ay isupf o∅) a → odef (UnionCF A f mf ay isupf o∅) (f a)
-inext {a} ua with (proj2 ua)
-... | ch-init fc = ⟪ proj2 (mf _ (proj1 ua))  , ch-init (fsuc _ fc )  ⟫
-... | ch-is-sup u u≤x is-sup fc = ⟪ proj2 (mf _ (proj1 ua)) ,  ch-is-sup u u≤x is-sup (fsuc _ fc) ⟫
-itotal : IsTotalOrderSet (UnionCF A f mf ay isupf o∅)
-itotal {a} {b} ca cb = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso uz01 where
-uz01 : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) )
-uz01 = chain-total A f mf ay isupf (proj2 ca) (proj2 cb)
-csupf : {z : Ordinal} → z o≤ o∅ → odef (UnionCF A f mf ay isupf z ) (isupf z)
-csupf {z} z≤0 = ⟪ asi , ch-is-sup o∅ o∅≤z uz02 (init asi refl) ⟫ where
-uz03 : {z : Ordinal } →  FClosure A f y z → (z ≡ isupf spi) ∨ (z << isupf spi)
-uz03 {z} fc with SUP.x<sup sp (subst (λ k → FClosure A f y k ) (sym &iso) fc )
-... | case1 eq = case1 ( begin
-z ≡⟨ sym &iso  ⟩
-& (* z) ≡⟨ cong (&) eq  ⟩
-spi  ∎ ) where open ≡-Reasoning
-... | case2 lt = case2 (subst (λ k → * z < k ) (sym *iso) lt )
-uz04 : {sup1 z1 : Ordinal} → isupf sup1 o< isupf spi → FClosure A f (isupf sup1) z1 → (z1 ≡ isupf spi) ∨ (z1 << isupf spi)
-uz04 {s} {z} s<spi fcz = ⊥-elim ( o<¬≡ refl s<spi )
-uz02 :  ChainP A f mf ay isupf o∅
-uz02 = record { fcy<sup = uz03 ; order = λ {s} {z} → {!!} ; supu=u = {!!} }
 SUP⊆ : { B C : HOD } → B ⊆' C → SUP A C → SUP A B
-SUP⊆ {B} {C} B⊆C sup = record { sup = SUP.sup sup ; A∋maximal = SUP.A∋maximal sup ; x<sup = λ lt → SUP.x<sup sup (B⊆C lt)    }
+SUP⊆ {B} {C} B⊆C sup = record { sup = SUP.sup sup ; as = SUP.as sup ; x<sup = λ lt → SUP.x<sup sup (B⊆C lt)    }
 --
 -- create all ZChains under o< x
 --
 pnext1 {a} ⟪ aa , ch-is-sup u u≤x is-sup fc ⟫ = ⟪ proj2 (mf a aa) , ch-is-sup u u≤x is-sup (fsuc _ fc ) ⟫
 -- if previous chain satisfies maximality, we caan reuse it
 --
 --  supf0 px is sup of UnionCF px , supf0 x is sup of UnionCF x
-no-extension : ¬  sp1 ≡ x → ZChain A f mf ay x
+no-extension : ¬  sp1 ≡ supf1 x → ZChain A f mf ay x
 no-extension ¬sp=x = record { supf = supf1 ;  sup = sup
-; initial = pinit1 ; chain∋init = pcy1 ; sup=u = sup=u ; supf-is-sup = {!!} ; csupf = {!!}
+; initial = pinit1 ; chain∋init = pcy1 ; sup=u = sup=u ; supf-is-sup = {!!} ; csupf = csupf
-;  chain⊆A = λ lt → proj1 lt ;  f-next = pnext1 ;  f-total = {!!} }  where
+;  chain⊆A = λ lt → proj1 lt ;  f-next = pnext1 ;  f-total = ptotal1 }  where
 UnionCF⊆ : {z : Ordinal } → z o≤ x →  UnionCF A f mf ay supf1 z ⊆' UnionCF A f mf ay supf0 x
 UnionCF⊆ {z} z≤x ⟪ au , ch-init fc ⟫ = ⟪ au , ch-init fc ⟫
-UnionCF⊆ {z} z≤x ⟪ au , ch-is-sup u1 u1≤x u1-is-sup (init  au1 refl) ⟫   = ⟪ au , ch-is-sup u1 ? ? (init ? ?) ⟫
+UnionCF⊆ {z} z≤x ⟪ au , ch-is-sup u1 u1≤z record { fcy<sup = fc<s ; order = o1 ; supu=u = sp=u }  (init  au1 refl) ⟫ = zc30 where
-UnionCF⊆ {z} z≤x ⟪ au , ch-is-sup u1 u1≤x u1-is-sup (fsuc xp fcu1) ⟫ with
+zc30 : odef (UnionCF A f mf ay supf0 x) (supf1 u1 )
-UnionCF⊆ {z} z≤x ⟪ A∋fc _ f mf fcu1 , ch-is-sup u1 u1≤x u1-is-sup fcu1 ⟫
+zc30 with trio< u1 px
+... | tri< a ¬b ¬c = ⟪ au , ch-is-sup u1 (OrdTrans u1≤z z≤x)  ? (init au1 refl) ⟫
+... | tri≈ ¬a b ¬c = ⟪ au , ch-is-sup u1 (OrdTrans u1≤z z≤x)  ? (init au1 refl) ⟫
+... | tri> ¬a ¬b px<u1 = ? where
+zc31 : u1 ≡ x
+zc31 with trio< u1 x
+... | tri< a ¬b ¬c = ⊥-elim (¬p<x<op ⟪ px<u1 , subst (λ k → u1 o< k) (sym (Oprev.oprev=x op)) a ⟫ )
+... | tri≈ ¬a b ¬c = b
+... | tri> ¬a ¬b c =  ⊥-elim (¬p<x<op ⟪ c , ordtrans≤-< u1≤z z≤x  ⟫ )
+UnionCF⊆ {z} z≤x ⟪ au , ch-is-sup u1 u1≤z u1-is-sup (fsuc xp fcu1) ⟫ with
+UnionCF⊆ {z} z≤x ⟪ A∋fc _ f mf fcu1 , ch-is-sup u1 u1≤z u1-is-sup fcu1 ⟫
+... | ⟪ aa , ch-init fc ⟫ = ⟪ proj2 ( mf _ aa ) , ch-init (fsuc _ fc) ⟫
+... | ⟪ aa , ch-is-sup u u≤x is-sup fc ⟫ = ⟪  proj2 ( mf _ aa ) , ch-is-sup u u≤x is-sup (fsuc _ fc) ⟫
+UnionCF⊆R : {z : Ordinal } → z o≤ x →  UnionCF A f mf ay supf0 z ⊆' UnionCF A f mf ay supf1 x
+UnionCF⊆R {z} z≤x ⟪ au , ch-init fc ⟫ = ⟪ au , ch-init fc ⟫
+UnionCF⊆R {z} z≤x ⟪ au , ch-is-sup u1 u1≤z u1-is-sup (init  au1 refl) ⟫
+= ⟪ au , ch-is-sup u1 (OrdTrans u1≤z z≤x) ? (init ? ?) ⟫
+UnionCF⊆R {z} z≤x ⟪ au , ch-is-sup u1 u1≤z u1-is-sup (fsuc xp fcu1) ⟫ with
+UnionCF⊆R {z} z≤x ⟪ A∋fc _ f mf fcu1 , ch-is-sup u1 u1≤z u1-is-sup fcu1 ⟫
 ... | ⟪ aa , ch-init fc ⟫ = ⟪ proj2 ( mf _ aa ) , ch-init (fsuc _ fc) ⟫
 ... | ⟪ aa , ch-is-sup u u≤x is-sup fc ⟫ = ⟪  proj2 ( mf _ aa ) , ch-is-sup u u≤x is-sup (fsuc _ fc) ⟫
 sup : {z : Ordinal} → z o≤ x → SUP A (UnionCF A f mf ay supf1 z)
 sup {z} z≤x with trio< z px
 ... | tri< a ¬b ¬c = SUP⊆ (UnionCF⊆ ? ) (ZChain.sup zc ? )
 sup=u {b} ab b<x is-sup with trio< b px
 ... | tri< a ¬b ¬c = ? where
 zc11 = ZChain.sup=u zc ab ? ?
 ... | tri≈ ¬a b ¬c = ?
 ... | tri> ¬a ¬b c = ?
+ptotal1 : IsTotalOrderSet pchain1
+ptotal1 {a} {b} ca cb = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso uz01 where
+uz01 : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) )
+uz01 = chain-total A f mf ay supf1 ( (proj2 ca)) ( (proj2 cb))
+csupf : {b : Ordinal} → b o≤ x → odef (UnionCF A f mf ay supf1 b) (supf1 b)
+csupf {b} b≤x with trio< b px | inspect supf1 b
+... | tri< a ¬b ¬c | record { eq = eq1 } = ⟪ ? , ? ⟫
+... | tri≈ ¬a b ¬c | record { eq = eq1 } = ⟪ ? , ? ⟫
+... | tri> ¬a ¬b px<b | record { eq = eq1 } = ⊥-elim ( ¬sp=x (subst (λ k → sp1 ≡ supf1 k ) (sym zc30) (sym eq1) )) where
+--   px< b ≤ x
+-- b ≡ x, supf x ≡ sp1 , ¬ x ≡ sp1
+zc30 : x ≡ b
+zc30 with osuc-≡< b≤x
+... | case1 eq = sym (eq)
+... | case2 b<x = ⊥-elim (¬p<x<op ⟪ px<b , subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) b<x ⟫ )
 zc4 : ZChain A f mf ay x
 zc4 with ODC.∋-p O A (* x)
 ... | no noax = no-extension {!!} -- ¬ A ∋ p, just skip
 ... | 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 x
 ... | case1 pr = no-extension {!!} -- we have previous A ∋ z < x , f z ≡ x, so chain ∋ f z ≡ x because of f-next
 ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A (ZChain.chain zc ) ax )
 ... | case1 is-sup = -- x is a sup of zc
-record {  supf = psupf1 ; chain⊆A = {!!} ; f-next = {!!} ; f-total = {!!} ; csupf = {!!} ; sup=u = {!!}
+record {  supf = psupf1 ; chain⊆A = {!!} ; f-next = {!!} ; f-total = {!!} ; csupf = csupf ; sup=u = {!!}
 ;  initial = {!!} ; chain∋init  = {!!} ; sup = {!!} ; supf-is-sup = {!!}   }  where
 supx : SUP A (UnionCF A f mf ay supf0 x)
-supx = record { sup = * x ; A∋maximal = subst (λ k → odef A k ) {!!} ax ; x<sup = {!!} }
+supx = record { sup = * x ; as = subst (λ k → odef A k ) {!!} ax ; x<sup = {!!} }
 spx = & (SUP.sup supx )
 x=spx : x ≡ spx
 x=spx = {!!}
 psupf1 : Ordinal → Ordinal
 psupf1 z with trio< z x
 ... | tri< a ¬b ¬c = ZChain.supf zc z
 ... | tri≈ ¬a b ¬c = x
 ... | tri> ¬a ¬b c = x
+csupf : {b : Ordinal} → b o≤ x → odef (UnionCF A f mf ay psupf1 b) (psupf1 b)
+csupf {b} b≤x with trio< b px | inspect psupf1 b
+... | tri< a ¬b ¬c | record { eq = eq1 } = ⟪ ? , ? ⟫
+... | tri≈ ¬a b ¬c | record { eq = eq1 } = ⟪ ? , ? ⟫
+... | tri> ¬a ¬b c | record { eq = eq1 } = ? where -- b ≡ x, supf x ≡ sp
+zc30 : x ≡ b
+zc30 with trio< x b
+... | tri< a ¬b ¬c = ?
+... | tri≈ ¬a b ¬c = b
+... | tri> ¬a ¬b c = ?
 ... | case2 ¬x=sup =  no-extension {!!} -- px is not f y' nor sup of former ZChain from y -- no extention
 ... | no lim = zc5 where
 sup=u {b} ab b<x is-sup with trio< b x
 ... | tri< a ¬b ¬c = ZChain.sup=u (pzc (osuc b)  (ob<x lim a))  ab ? record { x<sup = {!!} }
 ... | tri≈ ¬a b ¬c = {!!}
 ... | tri> ¬a ¬b c = {!!}
 csupf : {z : Ordinal} → z o≤ x → odef (UnionCF A f mf ay supf1 z) (supf1 z)
-csupf {z} z<x with trio< z x
+csupf {z} z≤x with trio< z x
 ... | tri< a ¬b ¬c = zc9 where
 zc9 : odef (UnionCF A f mf ay supf1 z)  (ZChain.supf  (pzc (osuc z) (ob<x lim a)) z)
 zc9 = {!!}
 zc8 : odef (UnionCF A f mf ay (supfu a) z)  (ZChain.supf  (pzc (osuc z) (ob<x lim a)) z)
 zc8 = ZChain.csupf  (pzc (osuc z) (ob<x lim a)) (o<→≤ <-osuc )
-... | tri≈ ¬a b ¬c = {!!} -- ⊥-elim (¬a z<x)
+... | tri≈ ¬a b ¬c = ?
-... | tri> ¬a ¬b c = {!!} -- ⊥-elim (¬a z<x)
+... | tri> ¬a ¬b x<z = ⊥-elim (o<¬≡ refl (ordtrans<-≤ x<z z≤x))
 zc5 : ZChain A f mf ay x
 zc5 with ODC.∋-p O A (* x)
 ... | no noax = no-extension {!!} -- ¬ A ∋ p, just skip
 ... | yes ax with ODC.p∨¬p O ( HasPrev A pchain ax f )
 SZ : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → {y : Ordinal} (ay : odef A y) → ZChain A f mf ay   (& A)
 SZ f mf {y} ay = TransFinite {λ z → ZChain A f mf ay   z  } (λ x → ind f mf ay x   ) (& A)
 zorn00 : Maximal A
 zorn00 with is-o∅ ( & HasMaximal )  -- we have no Level (suc n) LEM
-... | no not = record { maximal = ODC.minimal O HasMaximal  (λ eq → not (=od∅→≡o∅ eq)) ; A∋maximal = zorn01 ; ¬maximal<x  = zorn02 } where
+... | no not = record { maximal = ODC.minimal O HasMaximal  (λ eq → not (=od∅→≡o∅ eq)) ; as = zorn01 ; ¬maximal<x  = zorn02 } where
 -- yes we have the maximal
 zorn03 :  odef HasMaximal ( & ( ODC.minimal O HasMaximal  (λ eq → not (=od∅→≡o∅ eq)) ) )
 zorn03 =  ODC.x∋minimal  O HasMaximal  (λ eq → not (=od∅→≡o∅ eq))   -- Axiom of choice
 zorn01 :  A ∋ ODC.minimal O HasMaximal (λ eq → not (=od∅→≡o∅ eq))
 zorn01  = proj1  zorn03
 ... | yes ¬Maximal = ⊥-elim ( z04 nmx 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) ) ⟫
+zc5 = ⟪  Maximal.as 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 (cf nmx) (cf-is-≤-monotonic nmx) as0 (& A)
 zorn04 = SZ (cf nmx) (cf-is-≤-monotonic nmx) (subst (λ k → odef A k ) &iso as )
 total : IsTotalOrderSet (ZChain.chain zorn04)
 total {a} {b} = zorn06  where
 zorn06 :  odef (ZChain.chain zorn04) (& a) → odef (ZChain.chain zorn04) (& b) → Tri (a < b) (a ≡ b) (b < a)

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

comparison src/zorn.agda @ 804:2d84411a636e