Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 851:717b8c3f55c9
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 05 Sep 2022 21:54:55 +0900 |
| parents | 2d8ce664ae31 |
| children | a28bb57c88e6 |
| files | src/zorn.agda |
| diffstat | 1 files changed, 87 insertions(+), 76 deletions(-) [+] |
line wrap: on
line diff
--- a/src/zorn.agda Mon Sep 05 14:04:41 2022 +0900 +++ b/src/zorn.agda Mon Sep 05 21:54:55 2022 +0900 @@ -738,19 +738,19 @@ supf0 = ZChain.supf zc - supf1 : Ordinal → Ordinal - supf1 z with trio< z px + supf1 : (px z : Ordinal) → Ordinal + supf1 px z with trio< z px ... | tri< a ¬b ¬c = ZChain.supf zc z ... | tri≈ ¬a b ¬c = ZChain.supf zc z ... | tri> ¬a ¬b c = ZChain.supf zc px pchain1 : HOD - pchain1 = UnionCF A f mf ay supf1 x + pchain1 = UnionCF A f mf ay (supf1 px) x 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)) + uz01 = chain-total A f mf ay (supf1 px) ( (proj2 ca)) ( (proj2 cb)) pchain⊆A1 : {y : Ordinal} → odef pchain1 y → odef A y pchain⊆A1 {y} ny = proj1 ny pnext1 : {a : Ordinal} → odef pchain1 a → odef pchain1 (f a) @@ -760,49 +760,48 @@ pinit1 {a} ⟪ aa , ua ⟫ with ua ... | ch-init fc = s≤fc y f mf fc ... | ch-is-sup u u≤x is-sup fc = ≤-ftrans (<=to≤ zc7) (s≤fc _ f mf fc) where - zc7 : y <= supf1 u + zc7 : y <= supf1 px u zc7 = ChainP.fcy<sup is-sup (init ay refl) pcy1 : odef pchain1 y pcy1 = ⟪ ay , ch-init (init ay refl) ⟫ - supf0=1 : {z : Ordinal } → z o≤ px → supf0 z ≡ supf1 z - supf0=1 {z} z≤px with trio< z px + supf0=1 : {px z : Ordinal } → z o≤ px → supf0 z ≡ supf1 px z + supf0=1 {px} {z} z≤px with trio< z px ... | tri< a ¬b ¬c = refl ... | tri≈ ¬a b ¬c = refl ... | tri> ¬a ¬b c = ⊥-elim ( o≤> z≤px c ) - supf∈A : {b : Ordinal} → b o≤ x → odef A (supf1 b) + supf∈A : {b : Ordinal} → b o≤ x → odef A (supf1 px b) supf∈A {b} b≤z with trio< b px ... | tri< a ¬b ¬c = proj1 ( ZChain.csupf zc (o<→≤ a )) ... | tri≈ ¬a b ¬c = proj1 ( ZChain.csupf zc (o≤-refl0 b )) ... | tri> ¬a ¬b c = proj1 ( ZChain.csupf zc o≤-refl ) - supf-mono : {a b : Ordinal } → a o≤ b → supf1 a o≤ supf1 b + supf-mono : {a b : Ordinal } → a o≤ b → supf1 px a o≤ supf1 px b supf-mono = ? - zc70 : HasPrev A pchain x f → ¬ xSUP pchain x - zc70 pr xsup = ? + fc0→1 : {px s z : Ordinal } → s o≤ px → FClosure A f (supf0 s) z → FClosure A f (supf1 px s) z + fc0→1 {px} {s} {z} s≤px fc = subst (λ k → FClosure A f k z ) (supf0=1 s≤px) fc - fc0→1 : {s z : Ordinal } → s o≤ px → FClosure A f (supf0 s) z → FClosure A f (supf1 s) z - fc0→1 {s} {z} s≤px fc = subst (λ k → FClosure A f k z ) (supf0=1 s≤px) fc + fc1→0 : {px s z : Ordinal } → s o≤ px → FClosure A f (supf1 px s) z → FClosure A f (supf0 s) z + fc1→0 {px} {s} {z} s≤px fc = subst (λ k → FClosure A f k z ) (sym (supf0=1 s≤px)) fc - fc1→0 : {s z : Ordinal } → s o≤ px → FClosure A f (supf1 s) z → FClosure A f (supf0 s) z - fc1→0 {s} {z} s≤px fc = subst (λ k → FClosure A f k z ) (sym (supf0=1 s≤px)) fc - - CP0→1 : {u : Ordinal } → u o≤ px → ChainP A f mf ay supf0 u → ChainP A f mf ay supf1 u - CP0→1 {u} u≤px cp = record { fcy<sup = fcy<sup ; order = order ; supu=u = trans (sym (supf0=1 u≤px)) (ChainP.supu=u cp) } where - fcy<sup : {z : Ordinal} → FClosure A f y z → (z ≡ supf1 u) ∨ (z << supf1 u ) + CP0→1 : {px u : Ordinal } → ({a b : Ordinal } → a o≤ b → supf1 px a o≤ supf1 px b) + → u o≤ px → ChainP A f mf ay supf0 u → ChainP A f mf ay (supf1 px) u + CP0→1 {px} {u} supf-mono u≤px cp = record { fcy<sup = fcy<sup ; order = order ; supu=u = trans (sym (supf0=1 u≤px)) (ChainP.supu=u cp) } where + fcy<sup : {z : Ordinal} → FClosure A f y z → (z ≡ supf1 px u) ∨ (z << supf1 px u ) fcy<sup {z} fc = subst ( λ k → (z ≡ k) ∨ (z << k )) (supf0=1 u≤px) ( ChainP.fcy<sup cp fc ) - order : {s : Ordinal} {z2 : Ordinal} → supf1 s o< supf1 u → FClosure A f (supf1 s) z2 → - (z2 ≡ supf1 u) ∨ (z2 << supf1 u) + order : {s : Ordinal} {z2 : Ordinal} → supf1 px s o< supf1 px u → FClosure A f (supf1 px s) z2 → + (z2 ≡ supf1 px u) ∨ (z2 << supf1 px u) order {s} {z2} s<u fc = subst (λ k → (z2 ≡ k) ∨ (z2 << k) ) (supf0=1 u≤px) ( ChainP.order cp ss<su (fc1→0 s≤px fc )) where s≤px : s o≤ px s≤px = ordtrans (supf-inject0 supf-mono s<u) u≤px ss<su : supf0 s o< supf0 u ss<su = subst₂ (λ j k → j o< k ) (sym (supf0=1 s≤px )) (sym (supf0=1 u≤px)) s<u - CP1→0 : {u : Ordinal } → u o≤ px → ChainP A f mf ay supf1 u → ChainP A f mf ay supf0 u - CP1→0 {u} u≤px cp = record { fcy<sup = fcy<sup ; order = order ; supu=u = trans (supf0=1 u≤px) (ChainP.supu=u cp) } where + CP1→0 : {px u : Ordinal } → ( {a b : Ordinal } → a o≤ b → supf1 px a o≤ supf1 px b) + → u o≤ px → ChainP A f mf ay (supf1 px) u → ChainP A f mf ay supf0 u + CP1→0 {px} {u} supf-mono u≤px cp = record { fcy<sup = fcy<sup ; order = order ; supu=u = trans (supf0=1 u≤px) (ChainP.supu=u cp) } where fcy<sup : {z : Ordinal} → FClosure A f y z → (z ≡ supf0 u) ∨ (z << supf0 u ) fcy<sup {z} fc = subst ( λ k → (z ≡ k) ∨ (z << k )) (sym (supf0=1 u≤px)) ( ChainP.fcy<sup cp fc ) order : {s : Ordinal} {z2 : Ordinal} → supf0 s o< supf0 u → FClosure A f (supf0 s) z2 → @@ -810,18 +809,18 @@ order {s} {z2} s<u fc = subst (λ k → (z2 ≡ k) ∨ (z2 << k) ) (sym (supf0=1 u≤px)) ( ChainP.order cp ss<su (fc0→1 s≤px fc )) where s≤px : s o≤ px s≤px = ordtrans (supf-inject0 (ZChain.supf-mono zc) s<u) u≤px - ss<su : supf1 s o< supf1 u + ss<su : supf1 px s o< supf1 px u ss<su = subst₂ (λ j k → j o< k ) (supf0=1 s≤px ) (supf0=1 u≤px) s<u - UnionCF0⊆1 : {z : Ordinal } → z o≤ px → UnionCF A f mf ay supf0 z ⊆' UnionCF A f mf ay supf1 z - UnionCF0⊆1 {z} z≤px ⟪ au , ch-init fc ⟫ = ⟪ au , ch-init fc ⟫ - UnionCF0⊆1 {z} z≤px ⟪ au , ch-is-sup u u≤z is-sup fc ⟫ = - ⟪ au , ch-is-sup u u≤z (CP0→1 (OrdTrans u≤z z≤px ) is-sup) (fc0→1 (OrdTrans u≤z z≤px ) fc) ⟫ + UnionCF0⊆1 : {px z : Ordinal } → ({a b : Ordinal } → a o≤ b → supf1 px a o≤ supf1 px b) → z o≤ px → UnionCF A f mf ay supf0 z ⊆' UnionCF A f mf ay (supf1 px) z + UnionCF0⊆1 {px} {z} supf-mono z≤px ⟪ au , ch-init fc ⟫ = ⟪ au , ch-init fc ⟫ + UnionCF0⊆1 {px} {z} supf-mono z≤px ⟪ au , ch-is-sup u u≤z is-sup fc ⟫ = + ⟪ au , ch-is-sup u u≤z (CP0→1 supf-mono (OrdTrans u≤z z≤px ) is-sup) (fc0→1 (OrdTrans u≤z z≤px ) fc) ⟫ - UnionCF1⊆0 : {z : Ordinal } → z o≤ px → UnionCF A f mf ay supf1 z ⊆' UnionCF A f mf ay supf0 z - UnionCF1⊆0 {z} z≤px ⟪ au , ch-init fc ⟫ = ⟪ au , ch-init fc ⟫ - UnionCF1⊆0 {z} z≤px ⟪ au , ch-is-sup u u≤z is-sup fc ⟫ = - ⟪ au , ch-is-sup u u≤z (CP1→0 (OrdTrans u≤z z≤px ) is-sup) + UnionCF1⊆0 : {px z : Ordinal } → ({a b : Ordinal } → a o≤ b → supf1 px a o≤ supf1 px b) → z o≤ px → UnionCF A f mf ay (supf1 px) z ⊆' UnionCF A f mf ay supf0 z + UnionCF1⊆0 {px} {z} supf-mono z≤px ⟪ au , ch-init fc ⟫ = ⟪ au , ch-init fc ⟫ + UnionCF1⊆0 {px} {z} supf-mono z≤px ⟪ au , ch-is-sup u u≤z is-sup fc ⟫ = + ⟪ au , ch-is-sup u u≤z (CP1→0 supf-mono (OrdTrans u≤z z≤px ) is-sup) (fc1→0 (OrdTrans u≤z z≤px ) fc) ⟫ -- zc100 : xSUP (UnionCF A f mf ay supf0 px) x → x ≡ sp1 @@ -832,41 +831,59 @@ -- supf0 px is sup of UnionCF px , supf0 x is sup of UnionCF x no-extension : ¬ xSUP (UnionCF A f mf ay supf0 px) x → ZChain A f mf ay x - no-extension ¬sp=x = record { supf = supf1 ; sup = sup ; supf-mono = supf-mono + no-extension ¬sp=x = record { supf = supf1 px ; sup = sup ; supf-mono = supf-mono ; initial = pinit1 ; chain∋init = pcy1 ; sup=u = sup=u ; supf-is-sup = sis ; csupf = csupf ; chain⊆A = λ lt → proj1 lt ; f-next = pnext1 ; f-total = ptotal1 } where pchain0=1 : pchain ≡ pchain1 pchain0=1 = ==→o≡ record { eq→ = zc10 ; eq← = zc11 } where zc10 : {z : Ordinal} → OD.def (od pchain) z → OD.def (od pchain1) z zc10 {z} ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫ - zc10 {z} ⟪ az , ch-is-sup u1 u1≤x u1-is-sup fc ⟫ = ⟪ az , ch-is-sup u1 (ordtrans u1≤x (osucc (pxo<x op))) (CP0→1 u1≤x u1-is-sup) (fc0→1 u1≤x fc) ⟫ + zc10 {z} ⟪ az , ch-is-sup u1 u1≤x u1-is-sup fc ⟫ = ⟪ az , ch-is-sup u1 (ordtrans u1≤x (osucc (pxo<x op))) (CP0→1 supf-mono u1≤x u1-is-sup) (fc0→1 u1≤x fc) ⟫ zc11 : {z : Ordinal} → OD.def (od pchain1) z → OD.def (od pchain) z zc11 {z} ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫ zc11 {z} ⟪ az , ch-is-sup u1 u1≤x u1-is-sup fc ⟫ with osuc-≡< u1≤x - ... | case1 eq = ⊥-elim (¬sp=x zcsup) where - x<sup : {w : Ordinal} → odef (UnionCF A f mf ay supf0 px) w → (w ≡ x) ∨ (w << x) - x<sup = ? - zc12 : supf1 x ≡ u1 - zc12 = subst (λ k → supf1 k ≡ u1) eq (ChainP.supu=u u1-is-sup) - zcsup : xSUP (UnionCF A f mf ay supf0 px) x - zcsup = record { ax = subst (λ k → odef A k) (trans zc12 eq) (supf∈A o≤-refl) ; is-sup = record { x<sup = x<sup } } - ... | case2 lt = ⟪ az , ch-is-sup u1 u1≤px (CP1→0 u1≤px u1-is-sup) (fc1→0 u1≤px fc) ⟫ where + ... | case2 lt = ⟪ az , ch-is-sup u1 u1≤px (CP1→0 supf-mono u1≤px u1-is-sup) (fc1→0 u1≤px fc) ⟫ where u1≤px : u1 o≤ px u1≤px = (subst (λ k → u1 o< k) (sym (Oprev.oprev=x op)) lt) - sup : {z : Ordinal} → z o≤ x → SUP A (UnionCF A f mf ay supf1 z) - sup {z} z≤x with trio< z px | inspect supf1 z - ... | tri< a ¬b ¬c | record { eq = eq1} = SUP⊆ (UnionCF1⊆0 (o<→≤ a)) (ZChain.sup zc (o<→≤ a) ) - ... | tri≈ ¬a b ¬c | record { eq = eq1} = SUP⊆ (UnionCF1⊆0 (o≤-refl0 b)) (ZChain.sup zc (o≤-refl0 b) ) - ... | tri> ¬a ¬b px<z | record { eq = eq1} = ? where + ... | case1 eq = ⊥-elim (¬sp=x zcsup) where + s1u=x : supf1 px u1 ≡ x + s1u=x = trans (ChainP.supu=u u1-is-sup) eq + zc13 : osuc px o< osuc u1 + zc13 = o≤-refl0 ( trans (Oprev.oprev=x op) (sym eq) ) + x<sup : {w : Ordinal} → odef (UnionCF A f mf ay supf0 px) w → (w ≡ x) ∨ (w << x) + x<sup {w} ⟪ az , ch-init {w} fc ⟫ = subst (λ k → (w ≡ k) ∨ (w << k)) s1u=x + ( ChainP.fcy<sup u1-is-sup {w} fc ) + x<sup {w} ⟪ az , ch-is-sup u u≤x is-sup fc ⟫ with osuc-≡< ( supf-mono (ordtrans u≤x zc13 )) + ... | case1 eq1 = ⊥-elim ( o<¬≡ zc14 u≤x ) where + zc14 : u ≡ osuc px + zc14 = begin + u ≡⟨ sym ( ChainP.supu=u is-sup) ⟩ + supf0 u ≡⟨ supf0=1 u≤x ⟩ + supf1 px u ≡⟨ eq1 ⟩ + supf1 px u1 ≡⟨ s1u=x ⟩ + x ≡⟨ sym (Oprev.oprev=x op) ⟩ + osuc px ∎ where open ≡-Reasoning + ... | case2 lt = subst (λ k → (w ≡ k) ∨ (w << k)) s1u=x ( ChainP.order u1-is-sup lt (fc0→1 u≤x fc) ) + zc12 : supf1 px x ≡ u1 + zc12 = subst (λ k → supf1 px k ≡ u1) eq (ChainP.supu=u u1-is-sup) + zcsup : xSUP (UnionCF A f mf ay supf0 px) x + zcsup = record { ax = subst (λ k → odef A k) (trans zc12 eq) (supf∈A o≤-refl) + ; is-sup = record { x<sup = x<sup } } + sup : {z : Ordinal} → z o≤ x → SUP A (UnionCF A f mf ay (supf1 px) z) + sup {z} z≤x with trio< z px | inspect (supf1 px) z + ... | tri< a ¬b ¬c | record { eq = eq1} = SUP⊆ (UnionCF1⊆0 supf-mono (o<→≤ a)) (ZChain.sup zc (o<→≤ a) ) + ... | tri≈ ¬a b ¬c | record { eq = eq1} = SUP⊆ (UnionCF1⊆0 supf-mono (o≤-refl0 b)) (ZChain.sup zc (o≤-refl0 b) ) + ... | tri> ¬a ¬b px<z | record { eq = eq1} = subst (λ k → SUP A k ) + (trans pchain0=1 (cong (λ k → UnionCF A f mf ay (supf1 px) k ) (sym zc30) )) (ZChain.sup zc o≤-refl ) where zc30 : z ≡ x zc30 with osuc-≡< z≤x ... | case1 eq = eq ... | case2 z<x = ⊥-elim (¬p<x<op ⟪ px<z , subst (λ k → z o< k ) (sym (Oprev.oprev=x op)) z<x ⟫ ) sup=u : {b : Ordinal} (ab : odef A b) → - b o≤ x → IsSup A (UnionCF A f mf ay supf1 b) ab → supf1 b ≡ b + b o≤ x → IsSup A (UnionCF A f mf ay (supf1 px) b) ab → (supf1 px) b ≡ b sup=u {b} ab b≤x is-sup with trio< b px - ... | tri< a ¬b ¬c = ZChain.sup=u zc ab (o<→≤ a) record { x<sup = λ lt → IsSup.x<sup is-sup (UnionCF0⊆1 (o<→≤ a) lt) } - ... | tri≈ ¬a b ¬c = ZChain.sup=u zc ab (o≤-refl0 b) record { x<sup = λ lt → IsSup.x<sup is-sup (UnionCF0⊆1 (o≤-refl0 b) lt) } + ... | tri< a ¬b ¬c = ZChain.sup=u zc ab (o<→≤ a) record { x<sup = λ lt → IsSup.x<sup is-sup (UnionCF0⊆1 supf-mono (o<→≤ a) lt) } + ... | tri≈ ¬a b ¬c = ZChain.sup=u zc ab (o≤-refl0 b) record { x<sup = λ lt → IsSup.x<sup is-sup (UnionCF0⊆1 supf-mono (o≤-refl0 b) lt) } ... | tri> ¬a ¬b px<b = ⊥-elim (¬sp=x zcsup ) where zc30 : x ≡ b zc30 with osuc-≡< b≤x @@ -876,10 +893,10 @@ zcsup with zc30 ... | refl = record { ax = ab ; is-sup = record { x<sup = λ {w} lt → IsSup.x<sup is-sup (subst (λ k → odef k w) pchain0=1 lt) } } - csupf : {b : Ordinal} → b o≤ x → odef (UnionCF A f mf ay supf1 (supf1 b)) (supf1 b) + csupf : {b : Ordinal} → b o≤ x → odef (UnionCF A f mf ay (supf1 px) (supf1 px b)) (supf1 px b) csupf {b} b≤x = ⟪ zc01 , ch-is-sup u o≤-refl record { fcy<sup = fcy<sup ; order = order ; supu=u = supu=u } fc ⟫ where - csupf0 : b o≤ px → odef (UnionCF A f mf ay supf0 (supf1 b)) (supf1 b) + csupf0 : b o≤ px → odef (UnionCF A f mf ay supf0 (supf1 px b)) (supf1 px b) csupf0 b≤px = subst (λ k → odef (UnionCF A f mf ay supf0 k) k ) (supf0=1 b≤px) ( ZChain.csupf zc b≤px ) zc04 : (b o≤ px ) ∨ (b ≡ x ) zc04 with trio< b px @@ -888,36 +905,33 @@ ... | tri> ¬a ¬b px<b with osuc-≡< b≤x ... | case1 eq = case2 eq ... | case2 b<x = ⊥-elim ( ¬p<x<op ⟪ px<b , subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) b<x ⟫ ) - zc01 : odef A (supf1 b) - zc01 with zc04 - ... | case1 le = proj1 ( csupf0 le ) - ... | case2 eq = ? -- subst (λ k → odef A k ) (sym (supf1=sp (o≤-refl0 (sym eq)))) (SUP.as sup1) - u = supf1 b - supu=u : supf1 u ≡ u + zc01 : odef A (supf1 px b) + zc01 = supf∈A b≤x + u = supf1 px b + supu=u : supf1 px u ≡ u supu=u with zc04 ... | case2 eq = begin - supf1 u ≡⟨ ? ⟩ + supf1 px u ≡⟨ ? ⟩ + supf0 px ≡⟨ ? ⟩ u ∎ where open ≡-Reasoning - ... | case1 le = subst (λ k → k ≡ u ) (supf0=1 zc05 ) ( ZChain.sup=u zc zc01 zc05 ? ) where + ... | case1 le = ? where zc06 : b o≤ px zc06 = le - zc05 : supf1 b o≤ px - zc05 = ? - zc02 : odef A (supf1 u) + zc02 : odef A (supf1 px u) zc02 = subst (λ k → odef A k ) (sym supu=u) zc01 - zc03 : supf1 u ≡ supf1 b + zc03 : supf1 px u ≡ supf1 px b zc03 = ? - fc : FClosure A f (supf1 u) (supf1 b) + fc : FClosure A f (supf1 px u) (supf1 px b) fc = init zc02 zc03 - fcy<sup : {z : Ordinal} → FClosure A f y z → (z ≡ supf1 u) ∨ (z << supf1 u) + fcy<sup : {z : Ordinal} → FClosure A f y z → (z ≡ supf1 px u) ∨ (z << supf1 px u) fcy<sup = ? - order : {s z1 : Ordinal} → supf1 s o< supf1 u → FClosure A f (supf1 s) z1 - → (z1 ≡ supf1 u) ∨ (z1 << supf1 u) + order : {s z1 : Ordinal} → supf1 px s o< supf1 px u → FClosure A f (supf1 px s) z1 + → (z1 ≡ supf1 px u) ∨ (z1 << supf1 px u) order = ? - sis : {z : Ordinal} (z≤x : z o≤ x) → supf1 z ≡ & (SUP.sup (sup z≤x)) + sis : {z : Ordinal} (z≤x : z o≤ x) → supf1 px z ≡ & (SUP.sup (sup z≤x)) sis {z} z≤x = zc40 where - zc40 : supf1 z ≡ & (SUP.sup (sup z≤x)) -- direct with statment causes error - zc40 with trio< z px | inspect supf1 z | inspect sup z≤x + zc40 : supf1 px z ≡ & (SUP.sup (sup z≤x)) -- direct with statment causes error + zc40 with trio< z px | inspect (supf1 px) z | inspect sup z≤x ... | tri< a ¬b ¬c | record { eq = eq1 } | record { eq = eq2 } = ? ... | tri≈ ¬a b ¬c | record { eq = eq1 } | record { eq = eq2 } = ? ... | tri> ¬a ¬b c | record { eq = eq1 } | record { eq = eq2 } = ? @@ -930,7 +944,7 @@ ... | 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 = {!!} ; supf-mono = {!!} + record { supf = supf1 x ; chain⊆A = {!!} ; f-next = {!!} ; f-total = {!!} ; csupf = {!!} ; sup=u = {!!} ; supf-mono = {!!} ; initial = {!!} ; chain∋init = {!!} ; sup = {!!} ; supf-is-sup = {!!} } where supx : SUP A (UnionCF A f mf ay supf0 x) supx = record { sup = * x ; as = subst (λ k → odef A k ) {!!} ax ; x<sup = {!!} } @@ -938,10 +952,7 @@ x=spx : x ≡ spx x=spx = sym &iso 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 + psupf1 z = supf1 x z 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 } = ⟪ {!!} , {!!} ⟫