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

comparison src/zorn.agda @ 1010:f80d525e6a6b

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Recursive record IChain
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 20 Nov 2022 17:33:10 +0900
parents 7c39cae23803
children 66154af40f89
comparison
equal deleted inserted replaced
1009:7c39cae23803 1010:f80d525e6a6b
1302 pzc : {z : Ordinal} → z o< x → ZChain A f mf ay z 1302 pzc : {z : Ordinal} → z o< x → ZChain A f mf ay z
1303 pzc {z} z<x = prev z z<x 1303 pzc {z} z<x = prev z z<x
1304 1304
1305 ysp = MinSUP.sup (ysup f mf ay) 1305 ysp = MinSUP.sup (ysup f mf ay)
1306 1306
1307 supf0 : Ordinal → Ordinal 1307 supfz : {z : Ordinal } → z o< x → Ordinal
1308 supf0 z with trio< z x 1308 supfz {z} z<x = ZChain.supf (pzc (ob<x lim z<x)) z
1309 ... | tri< a ¬b ¬c = ZChain.supf (pzc (ob<x lim a)) z 1309
1310 ... | tri≈ ¬a b ¬c = ysp 1310 record IChain (supfz : {z : Ordinal } → z o< x → Ordinal) (z : Ordinal ) : Set n where
1311 ... | tri> ¬a ¬b c = ysp 1311 field
1312 1312 i : Ordinal
1313 pchain : HOD 1313 i<x : i o< x
1314 pchain = UnionCF A f mf ay supf0 x 1314 fc : FClosure A f (supfz i<x) z
1315 1315
1316 ptotal0 : IsTotalOrderSet pchain 1316 pchainx : HOD
1317 ptotal0 {a} {b} ca cb = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso uz01 where 1317 pchainx = record { od = record { def = λ z → IChain supfz z } ; odmax = & A ; <odmax = zc00 } where
1318 zc00 : {z : Ordinal } → IChain supfz z → z o< & A
1319 zc00 {z} ic = z09 ( A∋fc (supfz (IChain.i<x ic)) f mf (IChain.fc ic) )
1320
1321 zeq : {xa xb z : Ordinal }
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
1324 zeq {xa} {xb} {z} xa<x xb<x xa≤xb z≤xa = spuf-unique A f mf ay xa≤xb
1325 (pzc xa<x) (pzc xb<x) z≤xa
1326
1327 ptotalx : IsTotalOrderSet pchainx
1328 ptotalx {a} {b} ia ib = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso uz01 where
1318 uz01 : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) ) 1329 uz01 : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) )
1319 uz01 = chain-total A f mf ay supf0 ( (proj2 ca)) ( (proj2 cb)) 1330 uz01 with trio< (IChain.i ia) (IChain.i ib)
1320 1331 ... | tri< a ¬b ¬c = ?
1321 usup : MinSUP A pchain 1332 ... | tri≈ ¬a b ¬c = ?
1322 usup = minsupP pchain (λ lt → proj1 lt) ptotal0 1333 ... | tri> ¬a ¬b c = ?
1334
1335 usup : MinSUP A pchainx
1336 usup = minsupP pchainx (λ lt → ? ) ptotalx
1323 spu = MinSUP.sup usup 1337 spu = MinSUP.sup usup
1324 1338
1325 supf1 : Ordinal → Ordinal 1339 supf1 : Ordinal → Ordinal
1326 supf1 z with trio< z x 1340 supf1 z with trio< z x
1327 ... | tri< a ¬b ¬c = ZChain.supf (pzc (ob<x lim a)) z 1341 ... | tri< a ¬b ¬c = ZChain.supf (pzc (ob<x lim a)) z
1328 ... | tri≈ ¬a b ¬c = spu 1342 ... | tri≈ ¬a b ¬c = spu
1329 ... | tri> ¬a ¬b c = spu 1343 ... | tri> ¬a ¬b c = spu
1330 1344
1331 pchain1 : HOD 1345 pchain : HOD
1332 pchain1 = UnionCF A f mf ay supf1 x 1346 pchain = UnionCF A f mf ay supf1 x
1333 1347
1334 zeq : {xa xb z : Ordinal } 1348 -- pchain ⊆ pchainx
1335 → (xa<x : xa o< x) → (xb<x : xb o< x) → xa o≤ xb → z o≤ xa 1349
1336 → ZChain.supf (pzc xa<x) z ≡ ZChain.supf (pzc xb<x) z 1350 ptotal : IsTotalOrderSet pchain
1337 zeq {xa} {xb} {z} xa<x xb<x xa≤xb z≤xa = spuf-unique A f mf ay xa≤xb 1351 ptotal {a} {b} ca cb = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso uz01 where
1338 (pzc xa<x) (pzc xb<x) z≤xa 1352 uz01 : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) )
1353 uz01 = chain-total A f mf ay supf1 ( (proj2 ca)) ( (proj2 cb))
1339 1354
1340 sf1=sf : {z : Ordinal } → (a : z o< x ) → supf1 z ≡ ZChain.supf (pzc (ob<x lim a)) z 1355 sf1=sf : {z : Ordinal } → (a : z o< x ) → supf1 z ≡ ZChain.supf (pzc (ob<x lim a)) z
1341 sf1=sf {z} z<x with trio< z x 1356 sf1=sf {z} z<x with trio< z x
1342 ... | tri< a ¬b ¬c = cong ( λ k → ZChain.supf (pzc (ob<x lim k)) z) o<-irr 1357 ... | tri< a ¬b ¬c = cong ( λ k → ZChain.supf (pzc (ob<x lim k)) z) o<-irr
1343 ... | tri≈ ¬a b ¬c = ⊥-elim (¬a z<x) 1358 ... | tri≈ ¬a b ¬c = ⊥-elim (¬a z<x)
1347 sf1=spu {z} x≤z with trio< z x 1362 sf1=spu {z} x≤z with trio< z x
1348 ... | tri< a ¬b ¬c = ⊥-elim (o≤> x≤z a) 1363 ... | tri< a ¬b ¬c = ⊥-elim (o≤> x≤z a)
1349 ... | tri≈ ¬a b ¬c = refl 1364 ... | tri≈ ¬a b ¬c = refl
1350 ... | tri> ¬a ¬b c = refl 1365 ... | tri> ¬a ¬b c = refl
1351 1366
1352 zc11 : {z : Ordinal } → (a : z o< x ) → odef pchain (ZChain.supf (pzc (ob<x lim a)) z) 1367 -- zc11 : {z : Ordinal } → (a : z o< x ) → odef pchain (ZChain.supf (pzc (ob<x lim a)) z)
1353 zc11 {z} z<x = ⟪ ZChain.asupf (pzc (ob<x lim z<x)) , ch-is-sup (ZChain.supf (pzc (ob<x lim z<x)) z) 1368 -- zc11 {z} z<x = ⟪ ZChain.asupf (pzc (ob<x lim z<x)) , ch-is-sup (ZChain.supf (pzc (ob<x lim z<x)) z)
1354 ? ? (init ? ?) ⟫ 1369 -- ? ? (init ? ?) ⟫
1355 1370
1356 sfpx<=spu : {z : Ordinal } → supf1 z <= spu 1371 sfpx<=spu : {z : Ordinal } → supf1 z <= spu
1357 sfpx<=spu {z} with trio< z x 1372 sfpx<=spu {z} with trio< z x
1358 ... | tri< a ¬b ¬c = MinSUP.x≤sup usup ? -- (init (ZChain.asupf (pzc (ob<x lim a)) ) refl ) 1373 ... | tri< a ¬b ¬c = MinSUP.x≤sup usup ? -- (init (ZChain.asupf (pzc (ob<x lim a)) ) refl )
1359 ... | tri≈ ¬a b ¬c = case1 refl 1374 ... | tri≈ ¬a b ¬c = case1 refl