Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 1479:22523e8af390
zorn fix start
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 30 Jun 2024 06:44:27 +0900 |
| parents | 623b2f792154 |
| children | ba406e2ba8af |
| files | src/zorn.agda |
| diffstat | 1 files changed, 22 insertions(+), 22 deletions(-) [+] |
line wrap: on
line diff
--- a/src/zorn.agda Sat Jun 29 21:08:29 2024 +0900 +++ b/src/zorn.agda Sun Jun 30 06:44:27 2024 +0900 @@ -227,8 +227,8 @@ -- open import Relation.Binary.Properties.Poset as Poset -IsTotalOrderSet : ( A : HOD ) → Set (Level.suc n) -IsTotalOrderSet A = {a b : HOD} → odef A (& a) → odef A (& b) → Tri (a < b) (a ≡ b) (b < a ) +IsTotalOrderSet : ( A : HOD ) → Set n +IsTotalOrderSet A = {a b : Ordinal } → odef A a → odef A b → Tri (* a < * b) (a ≡ b) (* b < * a ) ⊆-IsTotalOrderSet : { A B : HOD } → B ⊆ A → IsTotalOrderSet A → IsTotalOrderSet B ⊆-IsTotalOrderSet {A} {B} B⊆A T ax ay = T (B⊆A ax) (B⊆A ay) @@ -407,13 +407,13 @@ -- -- supf is minsup, so its UniofCF are equal, these are equal -- - supfeq : {a b : Ordinal } → a o≤ z → b o≤ z → UnionCF A f ay supf a ≡ UnionCF A f ay supf b → supf a ≡ supf b + supfeq : {a b : Ordinal } → a o≤ z → b o≤ z → UnionCF A f ay supf a =h= UnionCF A f ay supf b → supf a ≡ supf b supfeq {a} {b} a≤z b≤z ua=ub with trio< (supf a) (supf b) ... | tri< sa<sb ¬b ¬c = ⊥-elim ( o≤> ( - IsMinSUP.minsup (is-minsup b≤z) asupf (λ {z} uzb → IsMinSUP.x≤sup (is-minsup a≤z) (subst (λ k → odef k z) (sym ua=ub) uzb)) ) sa<sb ) + IsMinSUP.minsup (is-minsup b≤z) asupf (λ {z} uzb → IsMinSUP.x≤sup (is-minsup a≤z) (eq← ua=ub uzb) )) sa<sb ) ... | tri≈ ¬a b ¬c = b ... | tri> ¬a ¬b sb<sa = ⊥-elim ( o≤> ( - IsMinSUP.minsup (is-minsup a≤z) asupf (λ {z} uza → IsMinSUP.x≤sup (is-minsup b≤z) (subst (λ k → odef k z) ua=ub uza)) ) sb<sa ) + IsMinSUP.minsup (is-minsup a≤z) asupf (λ {z} uza → IsMinSUP.x≤sup (is-minsup b≤z) (eq→ ua=ub uza) )) sb<sa ) -- -- supf a over b and supf a is not included in UnionCF a nor UnionCF b, so UnionCF b is equal to the UnionCF a @@ -438,7 +438,7 @@ x≤supfx→¬sa<sa : {a b : Ordinal } → b o≤ z → b o≤ supf a → ¬ (supf a o< supf b ) x≤supfx→¬sa<sa {a} {b} b≤z b≤sa sa<sb = ⊥-elim ( o<¬≡ z27 sa<sb ) where -- x o≤ supf a ∧ supf a o< supf b → ⊥, because it defines the same UnionCF z27 : supf a ≡ supf b - z27 = supfeq (ordtrans (supf-inject sa<sb) b≤z) b≤z ? -- ( union-max b≤sa b≤z sa<sb) + z27 = supfeq (ordtrans (supf-inject sa<sb) b≤z) b≤z ( union-max b≤sa b≤z sa<sb) order : {a b w : Ordinal } → b o≤ z → supf a o< supf b → FClosure A f (supf a) w → w ≤ supf b order {a} {b} {w} b≤z sa<sb fc = IsMinSUP.x≤sup (is-minsup b≤z) (cfcs (supf-inject sa<sb) b≤z sa<b fc) where @@ -465,38 +465,38 @@ f-total : IsTotalOrderSet chain f-total {a} {b} ⟪ uaa , ch-is-sup ua sua<x sua=ua fca ⟫ ⟪ uab , ch-is-sup ub sub<x sub=ub fcb ⟫ = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) ? ? fc-total where - fc-total : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) ) + fc-total : Tri (* a < * b) (a ≡ b) (* b < * a ) fc-total with trio< ua ub ... | tri< a₁ ¬b ¬c with ≤-ftrans (order (o<→≤ sub<x) (subst₂ (λ j k → j o< k) (sym sua=ua) (sym sub=ub) a₁) fca ) (s≤fc (supf ub) f mf fcb ) - ... | case1 eq1 = tri≈ (λ lt → ⊥-elim (<-irr (case1 (sym ct00)) lt)) ct00 (λ lt → ⊥-elim (<-irr (case1 ct00) lt)) where - ct00 : * (& a) ≡ * (& b) - ct00 = cong (*) eq1 - ... | case2 a<b = tri< a<b (λ eq → <-irr (case1 (sym eq)) a<b ) (λ lt → <-irr (case2 a<b ) lt) + ... | case1 eq1 = tri≈ (λ lt → ⊥-elim (<-irr (case1 (sym ?)) lt)) ? (λ lt → ⊥-elim (<-irr (case1 ?) lt)) where + ct00 : a ≡ b + ct00 = ? + ... | case2 a<b = tri< a<b (λ eq → <-irr (case1 ?) a<b ) (λ lt → <-irr (case2 a<b ) lt) fc-total | tri≈ _ refl _ = fcn-cmp _ f mf fca fcb fc-total | tri> ¬a ¬b c with ≤-ftrans (order (o<→≤ sua<x) (subst₂ (λ j k → j o< k) (sym sub=ub) (sym sua=ua) c) fcb ) (s≤fc (supf ua) f mf fca ) - ... | case1 eq1 = tri≈ (λ lt → ⊥-elim (<-irr (case1 (sym ct00)) lt)) ct00 (λ lt → ⊥-elim (<-irr (case1 ct00) lt)) where - ct00 : * (& a) ≡ * (& b) - ct00 = cong (*) (sym eq1) + ... | case1 eq1 = tri≈ (λ lt → ⊥-elim (<-irr (case1 (sym ?)) lt)) ? (λ lt → ⊥-elim (<-irr (case1 ?) lt)) where + ct00 : a ≡ b + ct00 = ? ... | case2 b<a = tri> (λ lt → <-irr (case2 b<a ) lt) (λ eq → <-irr (case1 eq) b<a ) b<a f-total {a} {b} ⟪ uaa , ch-init fca ⟫ ⟪ uab , ch-is-sup ub sub<x sub=ub fcb ⟫ = ft00 where - ft01 : (& a) ≤ (& b) → Tri ( a < b) ( a ≡ b) ( b < a ) + ft01 : a ≤ b → Tri ( * a < * b) ( a ≡ b) ( * b < * a ) ft01 (case1 eq) = tri≈ (λ lt → ⊥-elim (<-irr (case1 (sym a=b)) lt)) a=b (λ lt → ⊥-elim (<-irr (case1 a=b) lt)) where a=b : a ≡ b - a=b = subst₂ (λ j k → j ≡ k ) ? ? (cong (*) eq) + a=b = ? -- subst₂ (λ j k → j ≡ k ) ? ? (cong (*) eq) ft01 (case2 lt) = tri< a<b (λ eq → <-irr (case1 (sym eq)) a<b ) (λ lt → <-irr (case2 a<b ) lt) where - a<b : a < b - a<b = subst₂ (λ j k → j < k ) ? ? lt - ft00 : Tri ( a < b) ( a ≡ b) ( b < a ) + a<b : * a < * b + a<b = ? -- subst₂ (λ j k → j < k ) ? ? lt + ft00 : Tri ( * a < * b) ( a ≡ b) ( * b < * a ) ft00 = ft01 (≤-ftrans (fcy<sup (o<→≤ sub<x) fca) (s≤fc {A} _ f mf fcb)) f-total {a} {b} ⟪ uaa , ch-is-sup ua sua<x sua=ua fca ⟫ ⟪ uab , ch-init fcb ⟫ = ft00 where - ft01 : (& b) ≤ (& a) → Tri ( a < b) ( a ≡ b) ( b < a ) + ft01 : (& b) ≤ (& a) → Tri ( * a < * b) ( a ≡ b) ( * b < * a ) ft01 (case1 eq) = tri≈ (λ lt → ⊥-elim (<-irr (case1 (sym a=b)) lt)) a=b (λ lt → ⊥-elim (<-irr (case1 a=b) lt)) where a=b : a ≡ b - a=b = subst₂ (λ j k → j ≡ k ) ? ? (cong (*) (sym eq)) + a=b = ? -- subst₂ (λ j k → j ≡ k ) ? ? (cong (*) (sym eq)) ft01 (case2 lt) = tri> (λ lt → <-irr (case2 b<a ) lt) (λ eq → <-irr (case1 eq) b<a ) b<a where b<a : b < a b<a = subst₂ (λ j k → j < k ) ? ? lt - ft00 : Tri ( a < b) ( a ≡ b) ( b < a ) + ft00 : Tri ( * a < * b) ( a ≡ b) ( * b < * a ) ft00 = ft01 (≤-ftrans (fcy<sup (o<→≤ sua<x) fcb) (s≤fc {A} _ f mf fca)) f-total {a} {b} ⟪ uaa , ch-init fca ⟫ ⟪ uab , ch-init fcb ⟫ = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) ? ? (fcn-cmp y f mf fca fcb )