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

comparison src/zorn.agda @ 596:f484cff027e4

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 14 Jun 2022 00:25:59 +0900
parents 96f377d87427
children 2595d2f6487b
comparison
equal deleted inserted replaced
595:96f377d87427 596:f484cff027e4
246 fc∨sup : FClosure A f p x ∨ ((a : Ordinal) → FClosure A f p a → (a ≡ x) ∨ (a << x) ) 246 fc∨sup : FClosure A f p x ∨ ((a : Ordinal) → FClosure A f p a → (a ≡ x) ∨ (a << x) )
247 f-min : (x1 : Ordinal) → ( (a : Ordinal) → FClosure A f p a → (a ≡ x1 ) ∨ (a << x1) ) → FClosure A f p x1 ∨ ( x o≤ x1 ) 247 f-min : (x1 : Ordinal) → ( (a : Ordinal) → FClosure A f p a → (a ≡ x1 ) ∨ (a << x1) ) → FClosure A f p x1 ∨ ( x o≤ x1 )
248 248
249 data Fc∨sup (A : HOD) {y : Ordinal} (ay : odef A y) ( f : Ordinal → Ordinal ) : (x : Ordinal) → Set n where 249 data Fc∨sup (A : HOD) {y : Ordinal} (ay : odef A y) ( f : Ordinal → Ordinal ) : (x : Ordinal) → Set n where
250 Finit : {z : Ordinal} → z ≡ y → Fc∨sup A ay f z 250 Finit : {z : Ordinal} → z ≡ y → Fc∨sup A ay f z
251 Fc : {p x : Ordinal} → p o< x → Fc∨sup A ay f p → FChain A f p x → Fc∨sup A ay f x 251 Fc : {p x : Ordinal} → p o< osuc x → Fc∨sup A ay f p → FChain A f p x → Fc∨sup A ay f x
252 252
253 record ZChain ( A : HOD ) (x : Ordinal) ( f : Ordinal → Ordinal ) ( z : Ordinal ) : Set (Level.suc n) where 253 record ZChain ( A : HOD ) (x : Ordinal) ( f : Ordinal → Ordinal ) ( z : Ordinal ) : Set (Level.suc n) where
254 field 254 field
255 chain : HOD 255 chain : HOD
256 chain⊆A : chain ⊆' A 256 chain⊆A : chain ⊆' A
582 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) } 582 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) }
583 u-initial : {z : Ordinal} → odef Uz z → * y ≤ * z 583 u-initial : {z : Ordinal} → odef Uz z → * y ≤ * z
584 u-initial {z} u = ZChain.initial ( uzc u ) (UZFChain.chain∋z u) 584 u-initial {z} u = ZChain.initial ( uzc u ) (UZFChain.chain∋z u)
585 u-chain∋x : odef Uz y 585 u-chain∋x : odef Uz y
586 u-chain∋x = record { u = y ; u<x = y<x ; chain∋z = ZChain.chain∋x (prev y y<x ay ) } 586 u-chain∋x = record { u = y ; u<x = y<x ; chain∋z = ZChain.chain∋x (prev y y<x ay ) }
587 u-mono : ( a b : Ordinal ) → b o< x → a o< b → (za : ZChain A y f a) (zb : ZChain A y f b) → ZChain.chain za ⊆' ZChain.chain zb 587 u-mono : ( a b : Ordinal ) → b o< x → a o< osuc b → (za : ZChain A y f a) (zb : ZChain A y f b) → ZChain.chain za ⊆' ZChain.chain zb
588 u-mono a b b<x = TransFinite {λ a → a o< b → (za : ZChain A y f a) (zb : ZChain A y f b) 588 u-mono a b b<x = TransFinite {λ a → a o< osuc b → (za : ZChain A y f a) (zb : ZChain A y f b)
589 → ZChain.chain za ⊆' ZChain.chain zb } uind a where 589 → ZChain.chain za ⊆' ZChain.chain zb } uind a where
590 open ZChain 590 open ZChain
591 uind : (a : Ordinal) 591 uind : (a : Ordinal)
592 → ((c : Ordinal) → c o< a → c o< b → (za : ZChain A y f c) (zb : ZChain A y f b) → chain za ⊆' chain zb) 592 → ((c : Ordinal) → c o< a → c o< osuc b → (za : ZChain A y f c) (zb : ZChain A y f b) → chain za ⊆' chain zb)
593 → a o< b → (za : ZChain A y f a) (zb : ZChain A y f b) → chain za ⊆' chain zb 593 → a o< osuc b → (za : ZChain A y f a) (zb : ZChain A y f b) → chain za ⊆' chain zb
594 uind a previ a<b za zb {i} zai = um01 where 594 uind a previ a≤b za zb {i} zai = um01 where
595 FC : Fc∨sup A (chain⊆A za (chain∋x za)) f i 595 FC : Fc∨sup A (chain⊆A za (chain∋x za)) f i
596 FC = fc∨sup za zai 596 FC = fc∨sup za zai
597 FCb : Fc∨sup A (chain⊆A zb (chain∋x zb)) f i 597 -- y≤fc : {a p : Ordinal} → Fc∨sup A p f i → * y ≤ * p
598 FCb = {!!} 598 -- y≤fc = {!!}
599 um01 : odef (chain zb) i 599 um01 : odef (chain zb) i
600 um01 with FC 600 um01 with FC
601 ... | Finit i=y = subst (λ k → odef (chain zb) k ) (sym i=y) ( chain∋x zb ) 601 ... | Finit i=y = subst (λ k → odef (chain zb) k ) (sym i=y) ( chain∋x zb )
602 ... | Fc {p} {i} p<i pFC fc with initial za zai 602 ... | Fc {p} {i} p≤i pFC fc with initial za zai
603 ... | case1 y=i = subst (λ k → odef (chain zb) k ) (subst₂ (λ j k → j ≡ k ) &iso &iso (cong (&) y=i)) ( chain∋x zb ) 603 ... | case1 y=i = subst (λ k → odef (chain zb) k ) (subst₂ (λ j k → j ≡ k ) &iso &iso (cong (&) y=i)) ( chain∋x zb )
604 ... | case2 y<i with (FChain.fc∨sup fc) 604 ... | case2 y<i with (FChain.fc∨sup fc)
605 ... | case1 fc = um02 i fc where 605 ... | case1 fc = um02 i fc where
606 um02 : (i : Ordinal) → FClosure A f p i → odef (chain zb) i 606 um02 : (i : Ordinal) → FClosure A f p i → odef (chain zb) i
607 um02 i (init ap i=p ) = {!!} 607 um02 i (init ap i=p ) = subst (λ k → odef (chain zb) k ) (sym i=p) (previ a {!!} {!!} za zb {!!} ) where
608 um02 i (fsuc j fc) = f-next zb ( um02 j fc ) 608 um02 i (fsuc j fc) = f-next zb ( um02 j fc )
609 ... | case2 sup = {!!} 609 ... | case2 sup = {!!}
610 -- is-max zb (chain∋x zb) {!!} (chain⊆A za zai) {!!} y<i where 610 -- is-max zb (chain∋x zb) {!!} (chain⊆A za zai) {!!} y<i where
611 -- pFC0 : Fc∨sup A (chain⊆A za (chain∋x za)) f p 611 -- pFC0 : Fc∨sup A (chain⊆A za (chain∋x za)) f p
612 -- pFC0 = pFC 612 -- pFC0 = pFC