Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 1400:1c7b0a040d9c
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Wed, 28 Jun 2023 14:02:57 +0900 |
| parents | 59346935f8a4 |
| children | 34f72406fcfd |
| files | src/cardinal.agda |
| diffstat | 1 files changed, 144 insertions(+), 141 deletions(-) [+] |
line wrap: on
line diff
--- a/src/cardinal.agda Wed Jun 28 08:56:28 2023 +0900 +++ b/src/cardinal.agda Wed Jun 28 14:02:57 2023 +0900 @@ -122,166 +122,169 @@ Bernstein : {a b : Ordinal } → Injection a b → Injection b a → OrdBijection a b -Bernstein {a} {b} iab iba = be00 where - be05 : {a b : Ordinal } → a o< b → Injection a b → Injection b a → ⊥ - be05 {a} {b} a<b iab iba = TransFinite0 {λ x → (b : Ordinal) → x o< b → Injection x b → Injection b x → ⊥ } - ind a b a<b iab iba where - ind :(x : Ordinal) → - ((y : Ordinal) → y o< x → (b : Ordinal) → y o< b → Injection y b → Injection b y → ⊥ ) → - (b : Ordinal) → x o< b → Injection x b → Injection b x → ⊥ - ind a prev b x<b (f @ record { i→ = fab ; iB = b∋fab ; inject = fab-inject }) - ( g @ record { i→ = fba ; iB = a∋fba ; inject = fba-inject })= ? where - - gf : Injection a a - gf = record { i→ = λ x ax → fba (fab x ax) (b∋fab x ax) ; iB = λ x ax → a∋fba _ (b∋fab x ax) - ; inject = λ x y ax ay eq → fab-inject _ _ ax ay ( fba-inject _ _ (b∋fab _ ax) (b∋fab _ ay) eq) } +Bernstein {a} {b} (f @ record { i→ = fab ; iB = b∋fab ; inject = fab-inject }) ( g @ record { i→ = fba ; iB = a∋fba ; inject = fba-inject }) + = record { fun← = ? + ; fun→ = ? + ; funB = ? + ; funA = ? + ; fiso← = ? + ; fiso→ = ? } + where + gf : Injection a a + gf = record { i→ = λ x ax → fba (fab x ax) (b∋fab x ax) ; iB = λ x ax → a∋fba _ (b∋fab x ax) + ; inject = λ x y ax ay eq → fab-inject _ _ ax ay ( fba-inject _ _ (b∋fab _ ax) (b∋fab _ ay) eq) } - data gfImage : (i : ℕ) (x : Ordinal) → Set n where - a-g : {x : Ordinal} → (ax : odef (* a) x ) → (¬ib : ¬ ( IsImage b a g x )) → gfImage 0 x - next-gf : {x y : Ordinal} → {i : ℕ} → (gfiy : gfImage i y )→ (ix : IsImage a a gf x) → gfImage (suc i) x + data gfImage : (i : ℕ) (x : Ordinal) → Set n where + a-g : {x : Ordinal} → (ax : odef (* a) x ) → (¬ib : ¬ ( IsImage b a g x )) → gfImage 0 x + next-gf : {x : Ordinal} → {i : ℕ} → (ix : IsImage a a gf x) → (gfiy : gfImage i (IsImage.y ix) ) → gfImage (suc i) x - a∋gfImage : (i : ℕ) → {x : Ordinal } → gfImage i x → odef (* a) x - a∋gfImage 0 {x} (a-g ax ¬ib) = ax - a∋gfImage (suc i) {x} (next-gf lt record { y = y ; ay = ay ; x=fy = x=fy }) = subst (λ k → odef (* a) k ) (sym x=fy) (a∋fba _ (b∋fab y ay) ) + a∋gfImage : (i : ℕ) → {x : Ordinal } → gfImage i x → odef (* a) x + a∋gfImage 0 {x} (a-g ax ¬ib) = ax + a∋gfImage (suc i) {x} (next-gf record { y = y ; ay = ay ; x=fy = x=fy } lt ) = subst (λ k → odef (* a) k ) (sym x=fy) (a∋fba _ (b∋fab y ay) ) - C : ℕ → HOD -- Image {& (C i)} {a} (gf i) does not work - C i = record { od = record { def = gfImage i } ; odmax = & (* a) ; <odmax = λ lt → odef< (a∋gfImage i lt) } + C : ℕ → HOD -- Image {& (C i)} {a} (gf i) does not work + C i = record { od = record { def = gfImage i } ; odmax = & (* a) ; <odmax = λ lt → odef< (a∋gfImage i lt) } - record CN (x : Ordinal) : Set n where - field - i : ℕ - gfix : gfImage i x + record CN (x : Ordinal) : Set n where + field + i : ℕ + gfix : gfImage i x - UC : HOD - UC = record { od = record { def = λ x → CN x } ; odmax = & (* a) ; <odmax = λ lt → odef< (a∋gfImage (CN.i lt) (CN.gfix lt)) } + UC : HOD + UC = record { od = record { def = λ x → CN x } ; odmax = & (* a) ; <odmax = λ lt → odef< (a∋gfImage (CN.i lt) (CN.gfix lt)) } - b-UC : HOD - b-UC = record { od = record { def = λ x → odef (* b) x ∧ (¬ CN x) } ; odmax = & (* b) ; <odmax = λ lt → odef< (proj1 lt) } - - -- UC ⊆ * a - -- f : UC → Image f UC is injection - -- g : Image f UC → UC is injection + b-UC : HOD + b-UC = record { od = record { def = λ x → odef (* b) x ∧ (¬ CN x) } ; odmax = & (* b) ; <odmax = λ lt → odef< (proj1 lt) } + + -- UC ⊆ * a + -- f : UC → Image f UC is injection + -- g : Image f UC → UC is injection - UC⊆a : * (& UC) ⊆ * a - UC⊆a {x} lt = a∋gfImage (CN.i be02) (CN.gfix be02) where - be02 : CN x - be02 = subst (λ k → odef k x) *iso lt + UC⊆a : * (& UC) ⊆ * a + UC⊆a {x} lt = a∋gfImage (CN.i be02) (CN.gfix be02) where + be02 : CN x + be02 = subst (λ k → odef k x) *iso lt - b-UC⊆b : * (& b-UC) ⊆ * b - b-UC⊆b {x} lt = proj1 ( subst (λ k → odef k x) *iso lt ) + b-UC⊆b : * (& b-UC) ⊆ * b + b-UC⊆b {x} lt = proj1 ( subst (λ k → odef k x) *iso lt ) - open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) - - fab-refl : {x : Ordinal } → {ax ax1 : odef (* a) x} → fab x ax ≡ fab x ax1 - fab-refl {x} {ax} {ax1} = cong (λ k → fab x k) ( HE.≅-to-≡ ( ∋-irr {* a} ax ax1 )) + open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) - fba-refl : {x : Ordinal } → {bx bx1 : odef (* b) x} → fba x bx ≡ fba x bx1 - fba-refl {x} {bx} {bx1} = cong (λ k → fba x k) ( HE.≅-to-≡ ( ∋-irr {* b} bx bx1 )) + fab-eq : {x y : Ordinal } → {ax : odef (* a) x} {ax1 : odef (* a) y} → x ≡ y → fab x ax ≡ fab y ax1 + fab-eq {x} {x} {ax} {ax1} refl = cong (λ k → fab x k) ( HE.≅-to-≡ ( ∋-irr {* a} ax ax1 )) - fab-eq : {x y : Ordinal } → {ax : odef (* a) x} {ax1 : odef (* a) y} → x ≡ y → fab x ax ≡ fab y ax1 - fab-eq {x} {x} {ax} {ax1} refl = cong (λ k → fab x k) ( HE.≅-to-≡ ( ∋-irr {* a} ax ax1 )) - - fba-eq : {x y : Ordinal } → {bx : odef (* b) x} {bx1 : odef (* b) y} → x ≡ y → fba x bx ≡ fba y bx1 - fba-eq {x} {x} {bx} {bx1} refl = cong (λ k → fba x k) ( HE.≅-to-≡ ( ∋-irr {* b} bx bx1 )) + fba-eq : {x y : Ordinal } → {bx : odef (* b) x} {bx1 : odef (* b) y} → x ≡ y → fba x bx ≡ fba y bx1 + fba-eq {x} {x} {bx} {bx1} refl = cong (λ k → fba x k) ( HE.≅-to-≡ ( ∋-irr {* b} bx bx1 )) - be10 : Injection (& b-UC) (& (Image (& b-UC) {a} (Injection-⊆ b-UC⊆b g) )) - be10 = record { i→ = be12 ; iB = be13 ; inject = be14 } where - be12 : (x : Ordinal) → odef (* (& b-UC)) x → Ordinal - be12 x lt = i→ g x (proj1 be02) where - be02 : odef (* b) x ∧ ( ¬ CN x ) - be02 = subst (λ k → odef k x) *iso lt - be13 : (x : Ordinal) (lt : odef (* (& b-UC)) x) → odef (* (& (Image (& b-UC) (Injection-⊆ b-UC⊆b g)))) (be12 x lt) - be13 x lt = subst (λ k → odef k (be12 x lt)) (sym *iso) record { y = x ; ay = subst (λ k → odef k x) (sym *iso) be02 ; x=fy = fba-refl } where - be02 : odef (* b) x ∧ ( ¬ CN x ) - be02 = subst (λ k → odef k x) *iso lt - be14 : (x y : Ordinal) (ltx : odef (* (& b-UC)) x) (lty : odef (* (& b-UC)) y) → be12 x ltx ≡ be12 y lty → x ≡ y - be14 x y ltx lty eq = inject g _ _ (proj1 (subst (λ k → odef k x) *iso ltx)) (proj1 (subst (λ k → odef k y) *iso lty)) eq + be10 : Injection (& b-UC) (& (Image (& b-UC) {a} (Injection-⊆ b-UC⊆b g) )) + be10 = record { i→ = be12 ; iB = be13 ; inject = be14 } where + be12 : (x : Ordinal) → odef (* (& b-UC)) x → Ordinal + be12 x lt = i→ g x (proj1 be02) where + be02 : odef (* b) x ∧ ( ¬ CN x ) + be02 = subst (λ k → odef k x) *iso lt + be13 : (x : Ordinal) (lt : odef (* (& b-UC)) x) → odef (* (& (Image (& b-UC) (Injection-⊆ b-UC⊆b g)))) (be12 x lt) + be13 x lt = subst (λ k → odef k (be12 x lt)) (sym *iso) record { y = x ; ay = subst (λ k → odef k x) (sym *iso) be02 ; x=fy = fba-eq refl } where + be02 : odef (* b) x ∧ ( ¬ CN x ) + be02 = subst (λ k → odef k x) *iso lt + be14 : (x y : Ordinal) (ltx : odef (* (& b-UC)) x) (lty : odef (* (& b-UC)) y) → be12 x ltx ≡ be12 y lty → x ≡ y + be14 x y ltx lty eq = inject g _ _ (proj1 (subst (λ k → odef k x) *iso ltx)) (proj1 (subst (λ k → odef k y) *iso lty)) eq - be11 : Injection (& (Image (& b-UC) {a} (Injection-⊆ b-UC⊆b g) )) (& b-UC) - be11 = record { i→ = be13 ; iB = be14 ; inject = be15 } where - be13 : (x : Ordinal) → odef (* (& (Image (& b-UC) (Injection-⊆ b-UC⊆b g)))) x → Ordinal - be13 x lt with subst (λ k → odef k x) *iso lt - ... | record { y = y ; ay = ay ; x=fy = x=fy } = y -- g⁻¹ x=fy : x ≡ fba y (proj1 (subst (λ k → OD.def (od k) y) *iso ay)) - be14 : (x : Ordinal) (lt : odef (* (& (Image (& b-UC) (Injection-⊆ b-UC⊆b g)))) x) → odef (* (& b-UC)) (be13 x lt) - be14 x lt with subst (λ k → odef k x) *iso lt - ... | record { y = y ; ay = ay ; x=fy = x=fy } = ay - be15 : (x y : Ordinal) (ltx : odef (* (& (Image (& b-UC) (Injection-⊆ b-UC⊆b g)))) x) - (lty : odef (* (& (Image (& b-UC) (Injection-⊆ b-UC⊆b g)))) y) → - be13 x ltx ≡ be13 y lty → x ≡ y - be15 x y ltx lty eq with subst (λ k → odef k x) *iso ltx | subst (λ k → odef k y) *iso lty - ... | record { y = ix ; ay = aix ; x=fy = x=fix } | record { y = iy ; ay = aiy ; x=fy = x=fiy } - = trans x=fix (trans ( fba-eq eq ) (sym x=fiy ) ) - - b-UC-iso0 : (x : Ordinal ) → (cx : odef (* (& b-UC)) x ) → i→ be11 ( i→ be10 x cx ) (iB be10 x cx) ≡ x - b-UC-iso0 x cx with subst (λ k → odef k ( i→ be10 x cx ) ) *iso (iB be10 x cx) - ... | record { y = y ; ay = ay ; x=fy = x=fy } = inject g _ _ (proj1 be03) (proj1 be02) (sym x=fy) where - be02 : odef (* b) x ∧ ( ¬ CN x ) - be02 = subst (λ k → odef k x) *iso cx - be03 : odef (* b) y ∧ ( ¬ CN y ) - be03 = subst (λ k → odef k y) *iso ay + be11 : Injection (& (Image (& b-UC) {a} (Injection-⊆ b-UC⊆b g) )) (& b-UC) + be11 = record { i→ = be13 ; iB = be14 ; inject = be15 } where + be13 : (x : Ordinal) → odef (* (& (Image (& b-UC) (Injection-⊆ b-UC⊆b g)))) x → Ordinal + be13 x lt with subst (λ k → odef k x) *iso lt + ... | record { y = y ; ay = ay ; x=fy = x=fy } = y -- g⁻¹ x=fy : x ≡ fba y (proj1 (subst (λ k → OD.def (od k) y) *iso ay)) + be14 : (x : Ordinal) (lt : odef (* (& (Image (& b-UC) (Injection-⊆ b-UC⊆b g)))) x) → odef (* (& b-UC)) (be13 x lt) + be14 x lt with subst (λ k → odef k x) *iso lt + ... | record { y = y ; ay = ay ; x=fy = x=fy } = ay + be15 : (x y : Ordinal) (ltx : odef (* (& (Image (& b-UC) (Injection-⊆ b-UC⊆b g)))) x) + (lty : odef (* (& (Image (& b-UC) (Injection-⊆ b-UC⊆b g)))) y) → + be13 x ltx ≡ be13 y lty → x ≡ y + be15 x y ltx lty eq with subst (λ k → odef k x) *iso ltx | subst (λ k → odef k y) *iso lty + ... | record { y = ix ; ay = aix ; x=fy = x=fix } | record { y = iy ; ay = aiy ; x=fy = x=fiy } + = trans x=fix (trans ( fba-eq eq ) (sym x=fiy ) ) + + b-UC-iso0 : (x : Ordinal ) → (cx : odef (* (& b-UC)) x ) → i→ be11 ( i→ be10 x cx ) (iB be10 x cx) ≡ x + b-UC-iso0 x cx with subst (λ k → odef k ( i→ be10 x cx ) ) *iso (iB be10 x cx) + ... | record { y = y ; ay = ay ; x=fy = x=fy } = inject g _ _ (proj1 be03) (proj1 be02) (sym x=fy) where + be02 : odef (* b) x ∧ ( ¬ CN x ) + be02 = subst (λ k → odef k x) *iso cx + be03 : odef (* b) y ∧ ( ¬ CN y ) + be03 = subst (λ k → odef k y) *iso ay - b-UC-iso1 : (x : Ordinal ) → (cx : odef (* (& (Image (& b-UC) {a} (Injection-⊆ b-UC⊆b g)))) x ) → i→ be10 ( i→ be11 x cx ) (iB be11 x cx) ≡ x - b-UC-iso1 x cx with subst (λ k → odef k x ) *iso cx - ... | record { y = y ; ay = ay ; x=fy = x=fy } = sym x=fy + b-UC-iso1 : (x : Ordinal ) → (cx : odef (* (& (Image (& b-UC) {a} (Injection-⊆ b-UC⊆b g)))) x ) → i→ be10 ( i→ be11 x cx ) (iB be11 x cx) ≡ x + b-UC-iso1 x cx with subst (λ k → odef k x ) *iso cx + ... | record { y = y ; ay = ay ; x=fy = x=fy } = sym x=fy - -- C n → f (C n) - fU : (x : Ordinal) → ( odef (* (& UC)) x) → Ordinal - fU x lt = be03 where - be02 : CN x - be02 = subst (λ k → odef k x) *iso lt - be03 : Ordinal - be03 with CN.i be02 | CN.gfix be02 - ... | zero | a-g {x} ax ¬ib = fab x ax - ... | suc i | next-gf gfiy record { y = y ; ay = ay ; x=fy = x=fy } - = fab x (subst (λ k → odef (* a) k) (sym x=fy) (a∋fba _ (b∋fab y ay) )) + -- C n → f (C n) + fU : (x : Ordinal) → ( odef (* (& UC)) x) → Ordinal + fU x lt = be03 where + be02 : CN x + be02 = subst (λ k → odef k x) *iso lt + be03 : Ordinal + be03 with CN.i be02 | CN.gfix be02 + ... | zero | a-g {x} ax ¬ib = fab x ax + ... | suc i | next-gf record { y = y ; ay = ay ; x=fy = x=fy } gfiy + = fab x (subst (λ k → odef (* a) k) (sym x=fy) (a∋fba _ (b∋fab y ay) )) - -- f (C n) → g (f (C n) ) ≡ C (suc i) - Uf : (x : Ordinal) → odef (* (& (Image (& UC) (Injection-⊆ UC⊆a f)))) x → Ordinal - Uf x lt with subst (λ k → odef k x ) *iso lt - ... | record { y = y ; ay = ay ; x=fy = x=fy } = y + -- f (C n) → g (f (C n) ) ≡ C (suc i) + Uf : (x : Ordinal) → odef (* (& (Image (& UC) (Injection-⊆ UC⊆a f)))) x → Ordinal + Uf x lt with subst (λ k → odef k x ) *iso lt + ... | record { y = y ; ay = ay ; x=fy = x=fy } = y - be04 : {x : Ordinal } → (cx : odef (* (& UC)) x) → odef (* (& (Image (& UC) (Injection-⊆ UC⊆a f)))) (fU x cx) - be04 {x} cx = subst (λ k → odef k (fU x cx) ) (sym *iso) be06 where - be02 : CN x - be02 = subst (λ k → odef k x) *iso cx - be06 : odef (Image (& UC) (Injection-⊆ UC⊆a f)) (fU x cx) - be06 with CN.i be02 | CN.gfix be02 - ... | zero | a-g ax ¬ib = record { y = x ; ay = subst (λ k → odef k x) (sym *iso) be02 ; x=fy = fab-refl } - ... | suc i | next-gf gfiy record { y = y ; ay = ay ; x=fy = x=fy } - = record { y = x ; ay = subst (λ k → odef k x) (sym *iso) be02 ; x=fy = fab-refl } + be04 : {x : Ordinal } → (cx : odef (* (& UC)) x) → odef (* (& (Image (& UC) (Injection-⊆ UC⊆a f)))) (fU x cx) + be04 {x} cx = subst (λ k → odef k (fU x cx) ) (sym *iso) be06 where + be02 : CN x + be02 = subst (λ k → odef k x) *iso cx + be06 : odef (Image (& UC) (Injection-⊆ UC⊆a f)) (fU x cx) + be06 with CN.i be02 | CN.gfix be02 + ... | zero | a-g ax ¬ib = record { y = x ; ay = subst (λ k → odef k x) (sym *iso) be02 ; x=fy = fab-eq refl } + ... | suc i | next-gf record { y = y ; ay = ay ; x=fy = x=fy } gfiy + = record { y = x ; ay = subst (λ k → odef k x) (sym *iso) be02 ; x=fy = fab-eq refl } + + UC-iso0 : (x : Ordinal ) → (cx : odef (* (& UC)) x ) → Uf ( fU x cx ) (be04 cx) ≡ x + UC-iso0 x cx = be03 where + be02 : CN x + be02 = subst (λ k → odef k x) *iso cx + be03 : Uf ( fU x cx ) (be04 cx) ≡ x + be03 with CN.i be02 | CN.gfix be02 | be04 cx + ... | zero | a-g ax ¬ib | cb with subst (λ k → odef k _ ) *iso cb | inspect (fU x) cx + ... | record { y = y ; ay = ay ; x=fy = x=fy } | record { eq = refl } = sym ( inject f _ _ ax (UC⊆a ay) x=fy ) + be03 | suc i | next-gf record { y = x1 ; ay = ax1 ; x=fy = x=fx1 } s | cb with + subst (λ k → odef k (fab x (subst (odef (* a)) (sym x=fx1) (a∋fba (fab x1 ax1) (b∋fab x1 ax1)))) ) *iso cb + ... | record { y = y ; ay = ay ; x=fy = x=fy } = sym ( inject f _ _ ax (UC⊆a ay) x=fy ) where + ax : odef (* a) x + ax = subst (λ k → odef (* a) k ) (sym x=fx1) ( a∋fba _ (b∋fab x1 ax1) ) - UC-iso0 : (x : Ordinal ) → (cx : odef (* (& UC)) x ) → Uf ( fU x cx ) (be04 cx) ≡ x - UC-iso0 x cx = be03 where - be02 : CN x - be02 = subst (λ k → odef k x) *iso cx - be03 : Uf ( fU x cx ) (be04 cx) ≡ x - be03 with CN.i be02 | CN.gfix be02 | be04 cx - ... | zero | a-g ax ¬ib | cb with subst (λ k → odef k _ ) *iso cb | inspect (fU x) cx - ... | record { y = y ; ay = ay ; x=fy = x=fy } | record { eq = refl } = sym ( inject f _ _ ax (UC⊆a ay) x=fy ) - be03 | suc i | next-gf s record { y = x1 ; ay = ax1 ; x=fy = x=fx1 } | cb with - subst (λ k → odef k (fab x (subst (odef (* a)) (sym x=fx1) (a∋fba (fab x1 ax1) (b∋fab x1 ax1)))) ) *iso cb - ... | record { y = y ; ay = ay ; x=fy = x=fy } = sym ( inject f _ _ ax (UC⊆a ay) x=fy ) where - ax : odef (* a) x - ax = subst (λ k → odef (* a) k ) (sym x=fx1) ( a∋fba _ (b∋fab x1 ax1) ) + be08 : {x : Ordinal } → (cx : odef (* (& (Image (& UC) (Injection-⊆ UC⊆a f)))) x) → odef (* (& UC)) (Uf x cx) + be08 {x} cx with subst (λ k → odef k x) *iso cx + ... | record { y = y ; ay = ay ; x=fy = x=fy } = ay + + UC-iso1 : (x : Ordinal ) → (cx : odef (* (& (Image (& UC) {b} (Injection-⊆ UC⊆a f)))) x ) → fU ( Uf x cx ) (be08 cx) ≡ x + UC-iso1 x cx = be14 where + be14 : fU ( Uf x cx ) (be08 cx) ≡ x + be14 with subst (λ k → odef k x) *iso cx + ... | record { y = y ; ay = ay ; x=fy = x=fy } with CN.i (subst (λ k → OD.def (od k) y) *iso ay) | CN.gfix (subst (λ k → OD.def (od k) y) *iso ay) + ... | 0 | a-g ax ¬ib = sym x=fy + ... | (suc i) | next-gf t ix = sym x=fy - be08 : {x : Ordinal } → (cx : odef (* (& (Image (& UC) (Injection-⊆ UC⊆a f)))) x) → odef (* (& UC)) (Uf x cx) - be08 {x} cx with subst (λ k → odef k x) *iso cx - ... | record { y = y ; ay = ay ; x=fy = x=fy } = ay - - UC-iso1 : (x : Ordinal ) → (cx : odef (* (& (Image (& UC) {b} (Injection-⊆ UC⊆a f)))) x ) → fU ( Uf x cx ) (be08 cx) ≡ x - UC-iso1 x cx = be14 where - be14 : fU ( Uf x cx ) (be08 cx) ≡ x - be14 with subst (λ k → odef k x) *iso cx - ... | record { y = y ; ay = ay ; x=fy = x=fy } with CN.i (subst (λ k → OD.def (od k) y) *iso ay) | CN.gfix (subst (λ k → OD.def (od k) y) *iso ay) - ... | 0 | a-g ax ¬ib = sym x=fy - ... | (suc i) | next-gf t ix = sym x=fy - - - be00 : OrdBijection a b - be00 with trio< a b - ... | tri< a ¬b ¬c = ⊥-elim ( be05 a iab iba ) - ... | tri≈ ¬a b ¬c = ordbij-refl b - ... | tri> ¬a ¬b c = ⊥-elim ( be05 c iba iab ) + Img∨ : (x : Ordinal) → odef (* b) x → odef (* (& (Image (& UC) (Injection-⊆ UC⊆a f)))) x ∨ odef (* (& (Image (& b-UC) (Injection-⊆ b-UC⊆b g)))) x + Img∨ x bx = be20 where + be20 : odef (* (& (Image (& UC) (Injection-⊆ UC⊆a f)))) x ∨ odef (* (& (Image (& b-UC) (Injection-⊆ b-UC⊆b g)))) x + be20 with ∨L＼X {* a} {UC} (a∋fba x bx) + ... | case1 uc = case1 (subst (λ k → odef k x) (sym *iso) be21 ) where + be21 : odef (Image (& UC) (Injection-⊆ UC⊆a f)) x + be21 with CN.i uc | CN.gfix uc + ... | 0 | a-g ax ¬ib = ⊥-elim (¬ib record { y = x ; ay = bx ; x=fy = refl } ) + ... | suc i | next-gf {x1} {y1} record { y = y ; ay = ay ; x=fy = x=fy } t + = record { y = y ; ay = subst (λ k → odef k y) (sym *iso) be25 ; x=fy = trans be24 (fab-eq refl) } where + be24 : x ≡ fab y ay + be24 = inject g _ _ bx (b∋fab y ay) x=fy + be25 : odef UC y + be25 = record { i = i ; gfix = t } + be20 | case2 ⟪ agx , ncn ⟫ = case2 (subst (λ k → odef k x) (sym *iso) be21 ) where + be21 : odef (Image (& b-UC) (Injection-⊆ b-UC⊆b g)) x + be21 = record { y = ? ; ay = ? ; x=fy = ? } _c<_ : ( A B : HOD ) → Set n A c< B = ¬ ( Injection (& A) (& B) )