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

comparison src/zorn.agda @ 1011:66154af40f89

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
IChain recursive record avoided
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 20 Nov 2022 17:44:21 +0900
parents f80d525e6a6b
children 6f6daf464616
comparison
equal deleted inserted replaced
1010:f80d525e6a6b 1011:66154af40f89
648 ¬maximal<x : {x : HOD} → A ∋ x → ¬ maximal < x -- A is Partial, use negative 648 ¬maximal<x : {x : HOD} → A ∋ x → ¬ maximal < x -- A is Partial, use negative
649 649
650 init-uchain : (A : HOD) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) {y : Ordinal } → (ay : odef A y ) 650 init-uchain : (A : HOD) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) {y : Ordinal } → (ay : odef A y )
651 { supf : Ordinal → Ordinal } { x : Ordinal } → odef (UnionCF A f mf ay supf x) y 651 { supf : Ordinal → Ordinal } { x : Ordinal } → odef (UnionCF A f mf ay supf x) y
652 init-uchain A f mf ay = ⟪ ay , ch-init (init ay refl) ⟫ 652 init-uchain A f mf ay = ⟪ ay , ch-init (init ay refl) ⟫
653
654 record IChain (A : HOD) ( f : Ordinal → Ordinal ) {x : Ordinal } (supfz : {z : Ordinal } → z o< x → Ordinal) (z : Ordinal ) : Set n where
655 field
656 i : Ordinal
657 i<x : i o< x
658 fc : FClosure A f (supfz i<x) z
653 659
654 Zorn-lemma : { A : HOD } 660 Zorn-lemma : { A : HOD }
655 → o∅ o< & A 661 → o∅ o< & A
656 → ( ( B : HOD) → (B⊆A : B ⊆' A) → IsTotalOrderSet B → SUP A B ) -- SUP condition 662 → ( ( B : HOD) → (B⊆A : B ⊆' A) → IsTotalOrderSet B → SUP A B ) -- SUP condition
657 → Maximal A 663 → Maximal A
1305 ysp = MinSUP.sup (ysup f mf ay) 1311 ysp = MinSUP.sup (ysup f mf ay)
1306 1312
1307 supfz : {z : Ordinal } → z o< x → Ordinal 1313 supfz : {z : Ordinal } → z o< x → Ordinal
1308 supfz {z} z<x = ZChain.supf (pzc (ob<x lim z<x)) z 1314 supfz {z} z<x = ZChain.supf (pzc (ob<x lim z<x)) z
1309 1315
1310 record IChain (supfz : {z : Ordinal } → z o< x → Ordinal) (z : Ordinal ) : Set n where
1311 field
1312 i : Ordinal
1313 i<x : i o< x
1314 fc : FClosure A f (supfz i<x) z
1315
1316 pchainx : HOD 1316 pchainx : HOD
1317 pchainx = record { od = record { def = λ z → IChain supfz z } ; odmax = & A ; <odmax = zc00 } where 1317 pchainx = record { od = record { def = λ z → IChain A f supfz z } ; odmax = & A ; <odmax = zc00 } where
1318 zc00 : {z : Ordinal } → IChain supfz z → z o< & A 1318 zc00 : {z : Ordinal } → IChain A f supfz z → z o< & A
1319 zc00 {z} ic = z09 ( A∋fc (supfz (IChain.i<x ic)) f mf (IChain.fc ic) ) 1319 zc00 {z} ic = z09 ( A∋fc (supfz (IChain.i<x ic)) f mf (IChain.fc ic) )
1320 1320
1321 zeq : {xa xb z : Ordinal } 1321 zeq : {xa xb z : Ordinal }
1322 → (xa<x : xa o< x) → (xb<x : xb o< x) → xa o≤ xb → z o≤ xa 1322 → (xa<x : xa o< x) → (xb<x : xb o< x) → xa o≤ xb → z o≤ xa
1323 → ZChain.supf (pzc xa<x) z ≡ ZChain.supf (pzc xb<x) z 1323 → ZChain.supf (pzc xa<x) z ≡ ZChain.supf (pzc xb<x) z