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

comparison src/zorn.agda @ 1030:40532b0ed230

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 Mon, 28 Nov 2022 18:53:10 +0900
parents 07ffcf16a3d4
children f276cf614fc5
comparison
equal deleted inserted replaced
1029:07ffcf16a3d4 1030:40532b0ed230
293 ct00 : * a ≡ * b 293 ct00 : * a ≡ * b
294 ct00 = ? -- trans (cong (*) eq) eq1 294 ct00 = ? -- trans (cong (*) eq) eq1
295 ... | case2 lt = tri< ct02 (λ eq → <-irr (case1 (sym eq)) ct02) (λ lt → <-irr (case2 ct02) lt) where 295 ... | case2 lt = tri< ct02 (λ eq → <-irr (case1 (sym eq)) ct02) (λ lt → <-irr (case2 ct02) lt) where
296 ct02 : * a < * b 296 ct02 : * a < * b
297 ct02 = ? -- subst (λ k → * k < * b ) (sym eq) lt 297 ct02 = ? -- subst (λ k → * k < * b ) (sym eq) lt
298 fc-total f mf supf {xa} {xb} {a} {b} ca cb | tri≈ a₁ ¬b ¬c = ?
298 fc-total f mf supf {xa} {xb} {a} {b} ca cb | tri< a₁ ¬b ¬c = ? 299 fc-total f mf supf {xa} {xb} {a} {b} ca cb | tri< a₁ ¬b ¬c = ?
299 300
300 301
301 ∈∧P→o< : {A : HOD } {y : Ordinal} → {P : Set n} → odef A y ∧ P → y o< & A 302 ∈∧P→o< : {A : HOD } {y : Ordinal} → {P : Set n} → odef A y ∧ P → y o< & A
302 ∈∧P→o< {A } {y} p = subst (λ k → k o< & A) &iso ( c<→o< (subst (λ k → odef A k ) (sym &iso ) (proj1 p ))) 303 ∈∧P→o< {A } {y} p = subst (λ k → k o< & A) &iso ( c<→o< (subst (λ k → odef A k ) (sym &iso ) (proj1 p )))
308 -- UnionCF A f supf x 309 -- UnionCF A f supf x
309 -- = record { od = record { def = λ z → odef A z ∧ UChain A f supf x z } ; odmax = & A ; <odmax = λ {y} sy → ∈∧P→o< sy } 310 -- = record { od = record { def = λ z → odef A z ∧ UChain A f supf x z } ; odmax = & A ; <odmax = λ {y} sy → ∈∧P→o< sy }
310 311
311 -- order : {x y w : Ordinal } → x o< y → FClosure A f (supf x) w → w <= supf y 312 -- order : {x y w : Ordinal } → x o< y → FClosure A f (supf x) w → w <= supf y
312 -- 313 --
314
315 data UChain { A : HOD } { f : Ordinal → Ordinal }
316 {supf : Ordinal → Ordinal} (x : Ordinal) : (z : Ordinal) → Set n where
317 ch-is-sup : (u : Ordinal) {z : Ordinal } (u<x : u o< x) (supu=u : supf u ≡ u) ( fc : FClosure A f (supf u) z ) → UChain x z
318
313 UnionCF : ( A : HOD ) ( f : Ordinal → Ordinal ) ( supf : Ordinal → Ordinal ) ( x : Ordinal ) → HOD 319 UnionCF : ( A : HOD ) ( f : Ordinal → Ordinal ) ( supf : Ordinal → Ordinal ) ( x : Ordinal ) → HOD
314 UnionCF A f supf x 320 UnionCF A f supf x
315 = record { od = record { def = λ z → odef A z ∧ ( { s : Ordinal} → s o< x → FClosure A f (supf s) z ) } ; 321 = record { od = record { def = λ z → odef A z ∧ UChain {A} {f} {supf} x z } ;
316 odmax = & A ; <odmax = λ {y} sy → ∈∧P→o< sy } 322 odmax = & A ; <odmax = λ {y} sy → ∈∧P→o< sy }
317 323
318 324
319 supf-inject0 : {x y : Ordinal } {supf : Ordinal → Ordinal } → (supf-mono : {x y : Ordinal } → x o≤ y → supf x o≤ supf y ) 325 supf-inject0 : {x y : Ordinal } {supf : Ordinal → Ordinal } → (supf-mono : {x y : Ordinal } → x o≤ y → supf x o≤ supf y )
320 → supf x o< supf y → x o< y 326 → supf x o< supf y → x o< y
350 356
351 357
352 chain-mono : {A : HOD} ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y) (supf : Ordinal → Ordinal ) 358 chain-mono : {A : HOD} ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y) (supf : Ordinal → Ordinal )
353 (supf-mono : {x y : Ordinal } → x o≤ y → supf x o≤ supf y ) {a b c : Ordinal} → a o≤ b 359 (supf-mono : {x y : Ordinal } → x o≤ y → supf x o≤ supf y ) {a b c : Ordinal} → a o≤ b
354 → odef (UnionCF A f supf a) c → odef (UnionCF A f supf b) c 360 → odef (UnionCF A f supf a) c → odef (UnionCF A f supf b) c
355 chain-mono f mf ay supf supf-mono {a} {b} {c} a≤b ⟪ uaa , ch-is-sup ⟫ = ? 361 chain-mono f mf ay supf supf-mono {a} {b} {c} a≤b ⟪ ua , ch-is-sup u u<x supu=u fc ⟫ = ⟪ ua , ch-is-sup u (ordtrans<-≤ u<x a≤b) supu=u fc ⟫
356 362
357 record ZChain ( A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) 363 record ZChain ( A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f)
358 {y : Ordinal} (ay : odef A y) ( z : Ordinal ) : Set (Level.suc n) where 364 {y : Ordinal} (ay : odef A y) ( z : Ordinal ) : Set (Level.suc n) where
359 field 365 field
360 supf : Ordinal → Ordinal 366 supf : Ordinal → Ordinal
366 order : {x y w : Ordinal } → x o< y → FClosure A f (supf x) w → w <= supf y 372 order : {x y w : Ordinal } → x o< y → FClosure A f (supf x) w → w <= supf y
367 373
368 asupf : {x : Ordinal } → odef A (supf x) 374 asupf : {x : Ordinal } → odef A (supf x)
369 supf-mono : {x y : Ordinal } → x o≤ y → supf x o≤ supf y 375 supf-mono : {x y : Ordinal } → x o≤ y → supf x o≤ supf y
370 supfmax : {x : Ordinal } → z o< x → supf x ≡ supf z 376 supfmax : {x : Ordinal } → z o< x → supf x ≡ supf z
377 supf0 : supf o∅ ≡ y
371 378
372 minsup : {x : Ordinal } → x o≤ z → MinSUP A (UnionCF A f supf x) 379 minsup : {x : Ordinal } → x o≤ z → MinSUP A (UnionCF A f supf x)
373 supf-is-minsup : {x : Ordinal } → (x≤z : x o≤ z) → supf x ≡ MinSUP.sup ( minsup x≤z ) 380 supf-is-minsup : {x : Ordinal } → (x≤z : x o≤ z) → supf x ≡ MinSUP.sup ( minsup x≤z )
374 381
375 chain : HOD 382 chain : HOD
384 s=ms {x} x≤z = &iso 391 s=ms {x} x≤z = &iso
385 392
386 chain∋init : odef chain y 393 chain∋init : odef chain y
387 chain∋init = ⟪ ay , ? ⟫ 394 chain∋init = ⟪ ay , ? ⟫
388 f-next : {a z : Ordinal} → odef (UnionCF A f supf z) a → odef (UnionCF A f supf z) (f a) 395 f-next : {a z : Ordinal} → odef (UnionCF A f supf z) a → odef (UnionCF A f supf z) (f a)
389 f-next {a} ⟪ aa , ch-is-sup ⟫ = ? 396 f-next {a} ⟪ aa , cp ⟫ = ?
390 initial : {z : Ordinal } → odef chain z → * y ≤ * z 397 initial : {z : Ordinal } → odef chain z → * y ≤ * z
391 initial {a} ⟪ aa , ua ⟫ = ? 398 initial {a} ⟪ aa , ua ⟫ = ?
392 f-total : IsTotalOrderSet chain 399 f-total : IsTotalOrderSet chain
393 f-total {a} {b} ca cb = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso uz01 where 400 f-total {a} {b} ca cb = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso uz01 where
394 uz01 : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) ) 401 uz01 : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) )
436 (subst (λ k → w <= k) (sym (supf-is-minsup x≤z)) ( MinSUP.x≤sup (minsup x≤z) uw) )) <-mono hp 443 (subst (λ k → w <= k) (sym (supf-is-minsup x≤z)) ( MinSUP.x≤sup (minsup x≤z) uw) )) <-mono hp
437 444
438 supf-idem : (mf< : <-monotonic-f A f) {b : Ordinal } → b o≤ z → supf b o≤ z → supf (supf b) ≡ supf b 445 supf-idem : (mf< : <-monotonic-f A f) {b : Ordinal } → b o≤ z → supf b o≤ z → supf (supf b) ≡ supf b
439 supf-idem mf< {b} b≤z sfb≤x = z52 where 446 supf-idem mf< {b} b≤z sfb≤x = z52 where
440 z54 : {w : Ordinal} → odef (UnionCF A f supf (supf b)) w → (w ≡ supf b) ∨ (w << supf b) 447 z54 : {w : Ordinal} → odef (UnionCF A f supf (supf b)) w → (w ≡ supf b) ∨ (w << supf b)
441 z54 {w} ⟪ aw , fc ⟫ = order ? ? where 448 z54 {w} ⟪ aw , ch-is-sup u u<x su=u fc ⟫ = order su<b fc where
442 u<b : supf b o< b 449 su<b : u o< b
443 u<b = ? 450 su<b = supf-inject (subst (λ k → k o< supf b ) (sym (su=u)) u<x )
444 z52 : supf (supf b) ≡ supf b 451 z52 : supf (supf b) ≡ supf b
445 z52 = sup=u asupf sfb≤x ⟪ record { x≤sup = z54 } , IsMinSUP→NotHasPrev asupf z54 ( λ ax → proj1 (mf< _ ax)) ⟫ 452 z52 = sup=u asupf sfb≤x ⟪ record { x≤sup = z54 } , IsMinSUP→NotHasPrev asupf z54 ( λ ax → proj1 (mf< _ ax)) ⟫
446 453
447 -- cp : (mf< : <-monotonic-f A f) {b : Ordinal } → b o≤ z → supf b o≤ z → ChainP A f supf (supf b) 454 -- cp : (mf< : <-monotonic-f A f) {b : Ordinal } → b o≤ z → supf b o≤ z → ChainP A f supf (supf b)
448 -- the condition of cfcs is satisfied, this is obvious 455 -- the condition of cfcs is satisfied, this is obvious