# HG changeset patch # User Shinji KONO # Date 1719093890 -32400 # Node ID aca42b19db4ce8039593b744b4f887fbe6a72a7f # Parent d0b4be1cab0d66fda14643cf77bc022f22b57f52 ... diff -r d0b4be1cab0d -r aca42b19db4c src/ZProduct.agda --- a/src/ZProduct.agda Sat Jun 22 19:23:56 2024 +0900 +++ b/src/ZProduct.agda Sun Jun 23 07:04:50 2024 +0900 @@ -427,6 +427,8 @@ i→ : (x : Ordinal ) → Ordinal iB : (x : Ordinal ) → ( lt : odef (* A) x ) → odef (* B) ( i→ x ) inject : (x y : Ordinal ) → ( ltx : odef (* A) x ) ( lty : odef (* A) y ) → i→ x ≡ i→ y → x ≡ y + -- + -- no i→-cong : (x y : Ordinal ) → ( ltx : odef (* A) x ) ( lty : odef (* A) y ) → x ≡ y → i→ x ≡ i→ y record HODBijection (A B : HOD ) : Set n where field @@ -436,6 +438,9 @@ funA : (x : Ordinal ) → ( lt : odef B x ) → odef A ( fun← x lt ) fiso← : (x : Ordinal ) → ( lt : odef A x ) → fun← ( fun→ x lt ) ( funB x lt ) ≡ x fiso→ : (x : Ordinal ) → ( lt : odef B x ) → fun→ ( fun← x lt ) ( funA x lt ) ≡ x + fcong→ : (x y : Ordinal ) → ( ltx : odef A x ) ( lty : odef A y ) → x ≡ y → fun→ x ltx ≡ fun→ y lty + fcong← : (x y : Ordinal ) → ( ltx : odef B x ) ( lty : odef B y ) → x ≡ y → fun← x ltx ≡ fun← y lty + hodbij-refl : { a b : HOD } → a ≡ b → HODBijection a b hodbij-refl {a} refl = record { @@ -445,6 +450,8 @@ ; funA = λ x lt → lt ; fiso← = λ x lt → refl ; fiso→ = λ x lt → refl + ; fcong→ = λ x y ltx lty eq → eq + ; fcong← = λ x y ltx lty eq → eq } hodbij-sym : { a b : HOD } → HODBijection a b → HODBijection b a @@ -455,6 +462,8 @@ ; funA = funB eq ; fiso← = fiso→ eq ; fiso→ = fiso← eq + ; fcong→ = fcong← eq + ; fcong← = fcong→ eq } where open HODBijection pj12 : (A B : HOD) {x : Ordinal} → (ab : odef (ZFP A B) x ) → diff -r d0b4be1cab0d -r aca42b19db4c src/cardinal.agda --- a/src/cardinal.agda Sat Jun 22 19:23:56 2024 +0900 +++ b/src/cardinal.agda Sun Jun 23 07:04:50 2024 +0900 @@ -116,25 +116,30 @@ Injection-∙ {a} {b} {c} f g = record { i→ = λ x → i→ g (i→ f x ) ; iB = λ x ax → iB g (i→ f x ) (iB f x ax) ; inject = λ x y ix iy eq → inject f _ _ ix iy (inject g _ _ (iB f x ix ) (iB f y iy ) eq ) } +WellDefined : {A : HOD} → (f : (x : Ordinal ) → odef A x → Ordinal ) → Set n +WellDefined {A} f = (x : Ordinal ) → ( lt1 lt2 : odef A x ) → f x lt1 ≡ f x lt2 + ==-bi : {A B C : HOD } → (ab : HODBijection A B) - → ( (x : Ordinal ) → ( lt1 lt2 : odef A x ) → fun→ ab x lt1 ≡ fun→ ab x lt2 ) - → ( (x : Ordinal ) → ( lt1 lt2 : odef B x ) → fun← ab x lt1 ≡ fun← ab x lt2 ) → (A =h= C → HODBijection C B) ∧ (B =h= C → HODBijection A C) -proj1 (==-bi {A} {B} {C} ab wld→ wld← ) a=c = record { +proj1 (==-bi {A} {B} {C} ab ) a=c = record { fun→ = λ x cx → fun→ ab x (eq← a=c cx) - ; fun← = λ x bx → fun← ab x bx + ; fun← = fun← ab ; funB = λ x cx → funB ab x (eq← a=c cx) ; funA = λ x cx → eq→ a=c (funA ab x cx) - ; fiso→ = λ x bx → trans (wld→ _ _ _) (fiso→ ab x bx) + ; fiso→ = λ x bx → trans (fcong→ ab _ _ _ _ refl ) (fiso→ ab x bx ) ; fiso← = λ x cx → fiso← ab x (eq← a=c cx) + ; fcong→ = λ x y cx cy eq → fcong→ ab x y (eq← a=c cx) (eq← a=c cy) eq + ; fcong← = fcong← ab } -proj2 (==-bi {A} {B} {C} ab wld→ wld←) b=c = record { +proj2 (==-bi {A} {B} {C} ab ) b=c = record { fun→ = λ x cx → fun→ ab x cx ; fun← = λ x bx → fun← ab x (eq← b=c bx) ; funB = λ x cx → eq→ b=c (funB ab x cx) ; funA = λ x cx → funA ab x (eq← b=c cx) ; fiso→ = λ x cx → fiso→ ab x (eq← b=c cx) - ; fiso← = λ x bx → trans (wld← _ _ _) (fiso← ab x bx) + ; fiso← = λ x bx → trans (fcong← ab _ _ _ _ refl ) (fiso← ab x bx ) + ; fcong→ = fcong→ ab + ; fcong← = λ x y cx cy eq → fcong← ab x y (eq← b=c cx) (eq← b=c cy) eq } -- @@ -142,14 +147,17 @@ -- A and C may overrap -- bi-∪ : {A B C D : HOD } → (ab : HODBijection A B) → (cd : HODBijection C D ) + → ((A ∩ C) =h= od∅) → ((B ∩ D) =h= od∅) → HODBijection (A ∪ C) (B ∪ D) -bi-∪ {A} {B} {C} {D} ab cd = record { +bi-∪ {A} {B} {C} {D} ab cd nac nbd = record { fun→ = fa ; fun← = fb ; funB = fa-isb ; funA = fb-isa ; fiso→ = faiso ; fiso← = fbiso + ; fcong→ = facong + ; fcong← = fbcong } where fa : (x : Ordinal) → odef (A ∪ C) x → Ordinal fa x (case1 a) = fun→ ab x a @@ -169,6 +177,17 @@ fbiso : (x : Ordinal) (lt : odef (A ∪ C) x) → fb (fa x lt) (fa-isb x lt) ≡ x fbiso x (case1 b) = fiso← ab x b fbiso x (case2 d) = fiso← cd x d + -- without fcong, we don't need nac and nbd + facong : (x y : Ordinal) (ltx : odef (A ∪ C) x) (lty : odef (A ∪ C) y) → x ≡ y → fa x ltx ≡ fa y lty + facong x .x (case1 x₁) (case1 x₂) refl = fcong→ ab x x x₁ x₂ refl + facong x .x (case1 x₁) (case2 x₂) refl = ⊥-elim (¬x<0 (eq→ nac ⟪ x₁ , x₂ ⟫)) + facong x .x (case2 x₁) (case1 x₂) refl = ⊥-elim (¬x<0 (eq→ nac ⟪ x₂ , x₁ ⟫)) + facong x .x (case2 x₁) (case2 x₂) refl = fcong→ cd x x x₁ x₂ refl + fbcong : (x y : Ordinal) (ltx : odef (B ∪ D) x) (lty : odef (B ∪ D) y) → x ≡ y → fb x ltx ≡ fb y lty + fbcong x .x (case1 x₁) (case1 x₂) refl = fcong← ab x x x₁ x₂ refl + fbcong x .x (case1 x₁) (case2 x₂) refl = ⊥-elim (¬x<0 (eq→ nbd ⟪ x₁ , x₂ ⟫)) + fbcong x .x (case2 x₁) (case1 x₂) refl = ⊥-elim (¬x<0 (eq→ nbd ⟪ x₂ , x₁ ⟫)) + fbcong x .x (case2 x₁) (case2 x₂) refl = fcong← cd x x x₁ x₂ refl -- -- f : A → B OrdBijection A (Image A f) @@ -180,7 +199,7 @@ Bernstein : {a b : Ordinal } → Injection a b → Injection b a → HODBijection (* a) (* b) Bernstein {a} {b} ( fi @ record { i→ = f ; iB = b∋f ; inject = f-inject }) ( gi @ record { i→ = g ; iB = a∋g ; inject = g-inject }) - = proj1 (==-bi (proj2 (==-bi (bi-∪ bi-UC bi-fUC) ? ? ) (==-sym b=fUC∨b-fUC)) ? ? ) (==-sym a=UC∨a-UC) + = proj1 (==-bi (proj2 (==-bi (bi-∪ bi-UC bi-fUC ? ? ) ) (==-sym b=fUC∨b-fUC)) ) (==-sym a=UC∨a-UC) where gf : Injection a a gf = record { i→ = λ x → g (f x ) ; iB = λ x ax → a∋g _ (b∋f x ax) @@ -230,8 +249,13 @@ be01 {x} (case1 gfx) = a∋gfImage gfx be01 {x} (case2 ngfx) = proj1 ngfx - wld-a : (x : Ordinal) (lt1 lt2 : odef (UC ∪ a-UC) x) → ? -- fa bi-UC bi-fUC x lt1 ≡ fa bi-UC bi-fUC x lt2 - wld-a = ? + exUC : (UC ∩ a-UC) =h= od∅ + exUC = record { eq→ = be00 ; eq← = be01 } where + be00 : {x : Ordinal} → odef (UC ∩ a-UC) x → odef od∅ x + be00 {x} ⟪ a-g ax₁ ¬ib , ⟪ ax , nuc ⟫ ⟫ = ? + be00 {x} ⟪ next-gf ix uc , ⟪ ax , nuc ⟫ ⟫ = ? + be01 : {x : Ordinal} → odef od∅ x → odef (UC ∩ a-UC) x + be01 {x} lt = ⊥-elim ( ¬x<0 lt ) FA : (x : Ordinal) → (ax : gfImage x) → Ordinal FA x ax = f x -- (a∋gfImage ax) @@ -261,10 +285,10 @@ ... | case2 nimg = ⊥-elim ( ncn (a-g ax nimg ) ) f-cong : {x y : Ordinal } → {ax : odef (* a) x} {ax1 : odef (* a) y} → x ≡ y → f x ≡ f y - f-cong {x} {x} {ax} {ax1} refl = ? -- cong (λ k → f x k) ( HE.≅-to-≡ ( ∋-irr {* a} ax ax1 )) + f-cong {x} {x} {ax} {ax1} refl = refl g-cong : {x y : Ordinal } → {bx : odef (* b) x} {bx1 : odef (* b) y} → x ≡ y → g x ≡ g y - g-cong {x} {x} {bx} {bx1} refl = ? -- cong (λ k → g x k) ( HE.≅-to-≡ ( ∋-irr {* b} bx bx1 )) + g-cong {x} {x} {bx} {bx1} refl = refl g⁻¹ : {x : Ordinal } → (ax : odef (* a) x) → (nc0 : IsImage b a gi x ) → Ordinal g⁻¹ {x} ax record { y = y ; ay = ay ; x=fy = x=fy } = y @@ -406,7 +430,7 @@ f2 = f -- postulate -- yes we have a proof but it is very slow b : HODBijection (Power S) S - b = subst₂ (λ j k → HODBijection j k) ? ? ( Bernstein f2 f1) -- this makes check very slow + b = ? -- subst₂ (λ j k → HODBijection j k) ? ? ( Bernstein f2 f1) -- this makes check very slow -- but postulate makes check weak eg. irrerevance of ∋ -- we have at least one element since Power S contains od∅