Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 1437:6cac0f746c83
clean up
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 02 Jul 2023 15:05:26 +0900 |
| parents | d6a0ecafff80 |
| children | 5d69ed581269 |
| files | src/cardinal.agda |
| diffstat | 1 files changed, 6 insertions(+), 248 deletions(-) [+] |
line wrap: on
line diff
--- a/src/cardinal.agda Sun Jul 02 14:39:47 2023 +0900 +++ b/src/cardinal.agda Sun Jul 02 15:05:26 2023 +0900 @@ -82,27 +82,14 @@ ay : odef a y x=fy : x ≡ f y ay -record IsInverseImage (a b : Ordinal) (iab : Injection a b ) (x y : Ordinal ) : Set n where - field - ax : odef (* a) x - x=fy : y ≡ i→ iab x ax - -InverseImage : {a : Ordinal} ( b : Ordinal ) → Injection a b → (y : Ordinal ) → HOD -InverseImage {a} b iab y = record { od = record { def = λ x → IsInverseImage a b iab x y } ; odmax = & (* a) ; <odmax = im00 } where - im00 : {x : Ordinal } → IsInverseImage a b iab x y → x o< & (* a) - im00 {x} record { ax = ax ; x=fy = x=fy } = odef< ax - Image⊆b : { a b : Ordinal } → (iab : Injection a b) → Image a iab ⊆ * b Image⊆b {a} {b} iab {x} record { y = y ; ay = ay ; x=fy = x=fy } = subst (λ k → odef (* b) k) (sym x=fy) (iB iab y ay) _=c=_ : ( A B : HOD ) → Set n A =c= B = HODBijection A B -c=→≡ : {A B : HOD} → A =c= B → (A ≡ ?) ∧ (B ≡ ?) -c=→≡ = ? - ≡→c= : {A B : HOD} → A ≡ B → A =c= B -≡→c= = ? +≡→c= eq = hodbij-refl eq open import BAlgebra O @@ -116,8 +103,6 @@ b-a⊆b {a} {b} {x} lt with subst (λ k → odef k x) *iso lt ... | ⟪ bx , ¬ax ⟫ = bx -open Data.Nat - Injection-⊆ : {a b c : Ordinal } → * c ⊆ * a → Injection a b → Injection c b Injection-⊆ {a} {b} {c} le f = record { i→ = λ x cx → i→ f x (le cx) ; iB = λ x cx → iB f x (le cx) ; inject = λ x y ix iy eq → inject f x y (le ix) (le iy) eq } @@ -126,9 +111,6 @@ Injection-∙ {a} {b} {c} f g = record { i→ = λ x ax → i→ g (i→ f x ax) (iB f x ax) ; iB = λ x ax → iB g (i→ f x ax) (iB f x ax) ; inject = λ x y ix iy eq → inject f x y ix iy (inject g (i→ f x ix) (i→ f y iy) (iB f x ix) (iB f y iy) eq) } -Exclusive : (A C : HOD) → Set n -Exclusive A C = ({x : Ordinal} → odef A x → ¬ odef C x) ∧ ({x : Ordinal} → odef C x → ¬ odef A x) - bi-∪ : {A B C D : HOD } → (ab : HODBijection A B) → (cd : HODBijection C D ) → HODBijection (A ∪ C) (B ∪ D) bi-∪ {A} {B} {C} {D} ab cd = record { @@ -194,11 +176,14 @@ FA : (x : Ordinal) → (ax : gfImage x) → Ordinal FA x ax = fab x (a∋gfImage ax) + b∋Uf1 : (x : Ordinal) → IsImage0 UC (* b) FA x → odef (* b) x + b∋Uf1 x record { y = y ; ay = ay ; x=fy = x=fy } = subst (λ k → odef (* b) k ) (sym x=fy) (b∋fab y (a∋gfImage ay)) + fUC : HOD - fUC = record { od = record { def = λ x → IsImage0 UC (* b) FA x } ; odmax = & (* a) ; <odmax = λ lt → ? } + fUC = record { od = record { def = λ x → IsImage0 UC (* b) FA x } ; odmax = & (* b) ; <odmax = λ {x} lt → odef< (b∋Uf1 x lt)} b-fUC : HOD - b-fUC = record { od = record { def = λ x → odef (* b) x ∧ (¬ IsImage0 UC (* b) FA x) } ; odmax = & (* a) ; <odmax = λ lt → ? } + b-fUC = record { od = record { def = λ x → odef (* b) x ∧ (¬ IsImage0 UC (* b) FA x) } ; odmax = & (* b) ; <odmax = λ lt → odef∧< lt } b=fUC∨b-fUC : * b ≡ fUC ∪ b-fUC b=fUC∨b-fUC = ==→o≡ record { eq→ = be00 ; eq← = be01 } where @@ -215,23 +200,6 @@ ... | case1 img = img ... | case2 nimg = ⊥-elim ( ncn (a-g ax nimg ) ) - aucimg : {x : Ordinal } → (cx : odef (* (& a-UC)) x ) → IsImage b a g x - aucimg {x} cx with subst (λ k → odef k x ) *iso cx - - ... | ⟪ ax , ncn ⟫ = nimg ax ncn - - -- 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 be02 where - be02 : gfImage x - be02 = subst (λ k → odef k x) *iso lt - - a-UC⊆a : * (& a-UC) ⊆ * a - a-UC⊆a {x} lt = proj1 ( subst (λ k → odef k x) *iso lt ) - open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) fab-eq : {x y : Ordinal } → {ax : odef (* a) x} {ax1 : odef (* a) y} → x ≡ y → fab x ax ≡ fab y ax1 @@ -240,11 +208,6 @@ 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 )) - UC∋gf : {y : Ordinal } → (uy : odef (* (& UC)) y ) → gfImage ( fba (fab y (UC⊆a uy) ) (b∋fab y (UC⊆a uy))) - UC∋gf {y} uy = next-gf record { y = _ ; ay = UC⊆a uy ; x=fy = fba-eq (fab-eq refl) } uc00 where - uc00 : gfImage y - uc00 = subst (λ k → odef k y) *iso uy - g⁻¹ : {x : Ordinal } → (ax : odef (* a) x) → (nc0 : IsImage b a g x ) → Ordinal g⁻¹ {x} ax record { y = y ; ay = ay ; x=fy = x=fy } = y @@ -261,12 +224,6 @@ g⁻¹-eq {x} ax ax' {record { y = y₁ ; ay = ay₁ ; x=fy = x=fy₁ }} {record { y = y ; ay = ay ; x=fy = x=fy }} = inject g _ _ ay₁ ay (trans (sym x=fy₁) x=fy ) - be15 : {x : Ordinal } → odef (* (& a-UC)) x → odef (* a) x - be15 {x} lt with subst (λ k → odef k x) *iso lt - ... | ⟪ ax , ncn ⟫ = ax - be16 : {x : Ordinal } → odef (* (& a-UC)) x → IsImage b a g x - be16 {x} lt with subst (λ k → odef k x) *iso lt - ... | ⟪ ax , ncn ⟫ = nimg ax ncn cc11-case2 : {x : Ordinal} (ax : odef (* a) x) → (ncn : ¬ gfImage x) @@ -280,32 +237,6 @@ fba y1 ay1 ≡⟨ sym (x=fy1) ⟩ x ∎ where open ≡-Reasoning - be10 : Injection (& a-UC) (b - (& (Image (& UC) (Injection-⊆ UC⊆a f) )) ) -- g⁻¹ x - be10 = record { i→ = λ x lt → g⁻¹ (be15 lt) (be16 lt) ; iB = be17 ; inject = be18 } where - be17 : (x : Ordinal) (lt : odef (* (& a-UC)) x) → odef (* (b - & (Image (& UC) (Injection-⊆ UC⊆a f)))) (g⁻¹ (be15 lt) (be16 lt)) - be17 x lt = subst ( λ k → odef k (g⁻¹ (be15 lt) (be16 lt))) (sym *iso) ⟪ be19 , - (λ img → be18 be14 (subst (λ k → odef k (g⁻¹ (be15 lt) (be16 lt))) *iso img) ) ⟫ where - be14 : odef a-UC x - be14 = subst (λ k → odef k x) *iso lt - be19 : odef (* b) (g⁻¹ (be15 lt) (be16 lt)) - be19 = b∋g⁻¹ (be15 lt) (be16 lt) - be18 : odef a-UC x → ¬ odef (Image (& UC) (Injection-⊆ UC⊆a f)) (g⁻¹ (be15 lt) (be16 lt)) - be18 ⟪ ax , ncn ⟫ record { y = y ; ay = ay ; x=fy = x=fy } = ncn ( subst (λ k → gfImage k) be113 (UC∋gf ay) ) where - be113 : fba (fab y (UC⊆a ay)) (b∋fab y (UC⊆a ay)) ≡ x - be113 = begin - fba (fab y (UC⊆a ay)) (b∋fab y (UC⊆a ay)) ≡⟨ fba-eq (sym x=fy) ⟩ - fba (g⁻¹ (be15 lt) (be16 lt)) be19 ≡⟨ g⁻¹-iso (be15 lt) (be16 lt) ⟩ - x ∎ where open ≡-Reasoning - be18 : (x y : Ordinal) (ltx : odef (* (& a-UC)) x) (lty : odef (* (& a-UC)) y) → g⁻¹ (be15 ltx) (be16 ltx) ≡ g⁻¹ (be15 lty) (be16 lty) → x ≡ y - be18 = ? - - be13 : (x : Ordinal) → odef (* (b - & (Image (& UC) (Injection-⊆ UC⊆a f)))) x → Ordinal - be13 x lt = fba x ( proj1 ( subst (λ k → odef k x) (*iso) lt )) - - be60 : {b x : Ordinal} → (bx : odef (* b) x) → (ncn : ( ¬ (odef ( Image (& UC) (Injection-⊆ UC⊆a f)) x)) ) - → odef (* b ＼ * (& (Image (& UC) (Injection-⊆ UC⊆a f)))) x - be60 {b} {x} bx ncn = ⟪ bx , subst (λ k → ¬ odef k x ) (sym *iso) ncn ⟫ - cc10-case2 : {x : Ordinal } → (bx : odef (* b) x ) → ¬ IsImage0 UC (* b) (λ x ax → fab x (a∋gfImage ax)) x → ¬ gfImage (fba x bx) @@ -313,118 +244,12 @@ cc10-case2 {x} bx nix (next-gf record { y = y ; ay = ay ; x=fy = x=fy } gfy) = nix record { y = _ ; ay = gfy ; x=fy = inject g _ _ bx (b∋fab y (a∋gfImage gfy)) (trans x=fy (fba-eq (fab-eq refl))) } - be11 : Injection (b - (& (Image (& UC) (Injection-⊆ UC⊆a f) ))) (& a-UC) -- g x - be11 = record { i→ = be13 ; iB = be14 ; inject = ? } where - be14 : (x : Ordinal) (lt : odef (* (b - & (Image (& UC) (Injection-⊆ UC⊆a f)))) x) → odef (* (& a-UC)) (be13 x lt) - be14 x lt = subst (λ k → odef k (be13 x lt)) (sym *iso) ⟪ a∋fba x ( proj1 ( subst (λ k → odef k x) (*iso) lt )) , be25 ⟫ where - be26 : ¬ (odef (* (& (Image (& UC) (Injection-⊆ UC⊆a f)))) x) - be26 = proj2 ( subst (λ k → odef k x) (*iso) lt ) - be25 : ¬ gfImage (be13 x lt) - be25 cn with cn - ... | a-g ax ¬ib = ⊥-elim (¬ib record { y = _ ; ay = proj1 ( subst (λ k → odef k x) (*iso) lt ) ; x=fy = refl } ) - ... | next-gf record { y = y ; ay = ay ; x=fy = x=fy } t - = ⊥-elim (be26 (subst (λ k → odef k x) (sym *iso) record { y = y - ; ay = subst (λ k → odef k y) (sym *iso) t ; x=fy = be17 })) where - be17 : x ≡ fab y (UC⊆a (subst (λ k → odef k y) (sym *iso) t)) - be17 = trans (inject g _ _ (proj1 ( subst (λ k → odef k x) (*iso) lt )) (b∋fab y ay) x=fy) (fab-eq refl) - - a-UC-iso0 : (x : Ordinal ) → (cx : odef (* (& a-UC)) x ) → i→ be11 ( i→ be10 x cx ) (iB be10 x cx) ≡ x - a-UC-iso0 x cx = trans (fba-eq refl) ( g⁻¹-iso (proj1 ( subst (λ k → odef k x) (*iso) cx )) (aucimg cx)) - - a-UC-iso1 : (x : Ordinal ) → (cx : odef (* (b - (& (Image (& UC) (Injection-⊆ UC⊆a f) )))) x ) → i→ be10 ( i→ be11 x cx ) (iB be11 x cx) ≡ x - a-UC-iso1 x cx with ODC.p∨¬p O ( IsImage b a g (fba x (proj1 ( subst (λ k → odef k x) (*iso) cx ))) ) - ... | case1 record { y = y ; ay = ay ; x=fy = x=fy } = sym ( inject g _ _ (proj1 ( subst (λ k → odef k x) (*iso) cx )) ay x=fy ) - ... | case2 ¬ism = ⊥-elim (¬ism record { y = x ; ay = proj1 ( subst (λ k → odef k x) (*iso) cx ) ; x=fy = refl }) - - a-UC-iso11 : (x : Ordinal ) → (cx : odef (* (b - (& (Image (& UC) (Injection-⊆ UC⊆a f) )))) x ) - → (ib : odef (* (& a-UC)) (fba x ( proj1 ( subst (λ k → odef k x) (*iso) cx )) )) - → i→ be10 ( i→ be11 x cx ) ib ≡ x - a-UC-iso11 x cx ib with ODC.p∨¬p O ( IsImage b a g (fba x (proj1 ( subst (λ k → odef k x) (*iso) cx ))) ) - ... | case1 record { y = y ; ay = ay ; x=fy = x=fy } = sym ( inject g _ _ (proj1 ( subst (λ k → odef k x) (*iso) cx )) ay x=fy ) - ... | case2 ¬ism = ⊥-elim (¬ism record { y = x ; ay = proj1 ( subst (λ k → odef k x) (*iso) cx ) ; x=fy = refl }) - - -- C n → f (C n) - fU : (x : Ordinal) → ( odef (* (& UC)) x) → Ordinal - fU x lt = be03 where - be02 : gfImage x - be02 = subst (λ k → odef k x) *iso lt - be03 : Ordinal - be03 with be02 - ... | a-g {x} ax ¬ib = fab x ax - ... | 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) )) - fU1 : (x : Ordinal) → odef UC x → Ordinal fU1 x gfx = fab x (a∋gfImage gfx) - -- 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 - - b∋Uf1 : (x : Ordinal) → IsImage0 UC (* b) FA x → odef (* b) x - b∋Uf1 x record { y = y ; ay = ay ; x=fy = x=fy } = subst (λ k → odef (* b) k ) (sym x=fy) (b∋fab y (a∋gfImage ay)) - Uf1 : (x : Ordinal) → IsImage0 UC (* b) FA x → Ordinal Uf1 x 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 : gfImage x - be02 = subst (λ k → odef k x) *iso cx - be06 : odef (Image (& UC) (Injection-⊆ UC⊆a f)) (fU x cx) - be06 with be02 - ... | a-g ax ¬ib = record { y = x ; ay = subst (λ k → odef k x) (sym *iso) be02 ; x=fy = fab-eq refl } - ... | 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 : gfImage x - be02 = subst (λ k → odef k x) *iso cx - be03 : Uf ( fU x cx ) (be04 cx) ≡ x - be03 with be02 | be04 cx - ... | 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 | 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) ) - - 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 subst (λ k → OD.def (od k) y) *iso ay - ... | a-g ax ¬ib = sym x=fy - ... | next-gf t ix = sym x=fy - - UC-iso11 : (x : Ordinal ) → (cx : odef (* (& (Image (& UC) {b} (Injection-⊆ UC⊆a f)))) x ) - → (ux : odef (* (& UC)) (Uf x cx)) → fU ( Uf x cx ) ux ≡ x - UC-iso11 x cx ux = subst (λ k → fU (Uf x cx) k ≡ x) ( HE.≅-to-≡ ( ∋-irr {* (& UC)} {_} (be08 cx) ux)) (UC-iso1 x cx) - - CC0 : (x : Ordinal) → Set n - CC0 x = gfImage x ∨ (¬ gfImage x) - - CC1 : (x : Ordinal) → Set n - CC1 x = IsImage0 UC (* b) FA x ∨ (¬ IsImage0 UC (* b) FA x) - - cc0 : (x : Ordinal) → CC0 x - cc0 x = ODC.p∨¬p O (gfImage x) - - cc1 : (x : Ordinal) → CC1 x - cc1 x = ODC.p∨¬p O (IsImage0 UC (* b) FA x) - - cc20 : {x : Ordinal } → (lt : odef (* b) x) → CC0 (fba x lt ) - cc20 {x} lt = cc0 (fba x lt) - - cc21 : {x : Ordinal } → (lt : odef (* a) x) → CC1 (fab x lt ) - cc21 {x} lt = cc1 (fab x lt) UC∋Uf1 : {x : Ordinal } → (lt : odef fUC x) → odef UC (Uf1 x lt ) UC∋Uf1 {x} record { y = y ; ay = ay ; x=fy = x=fy } = ay @@ -471,73 +296,6 @@ ; fiso→ = λ x lt → fUC-iso0 lt } - -- - -- h : * a → * b - -- h⁻¹ : * b → * a - -- - -- it have to accept any alement in a or b - -- it is handle by different function fU or gU with exclusive conditon CC0 (p ∨ ¬ p) - -- in HODBijection record, LEM rules are used - -- but we cannot use LEM in second function call on iso parts. - -- so we have to do some devices. - -- - -- otherwise not strict positive on gfImage error will happen - - h : {x : Ordinal } → (ax : odef (* a) x) → CC0 x → Ordinal - h {x} ax (case1 cn) = fU1 x cn - h {x} ax (case2 ncn) = g⁻¹ ax (nimg ax ncn) - - h⁻¹ : {x : Ordinal } → (bx : odef (* b) x) → CC1 x → Ordinal - h⁻¹ {x} bx ( case1 cn) = Uf1 x cn -- x ≡ f y - h⁻¹ {x} bx ( case2 ncn) = fba x bx - - cc10 : {x : Ordinal} → (bx : odef (* b) x) → (cc1 : CC1 x ) → CC0 (h⁻¹ bx cc1 ) - cc10 {x} bx (case1 record { y = y ; ay = ay ; x=fy = x=fy }) = - case1 (next-gf record { y = _ ; ay = a∋gfImage ay ; x=fy = ? } ay ) - cc10 {x} bx (case2 x₁) = case2 (cc10-case2 bx x₁ ) - - cc11 : {x : Ordinal} → (ax : odef (* a) x) → (cc0 : CC0 x ) → CC1 (h ax cc0 ) - cc11 {x} ax (case1 x₁) = case1 record {y = _ ; ay = x₁ ; x=fy = refl } - cc11 {x} ax (case2 x₁) = case2 (cc11-case2 ax x₁) - - be70 : (x : Ordinal) (lt : odef (* a) x) → (or : CC0 x ) → odef (* b) (h lt or ) - be70 x ax ( case1 cn ) = b∋fab x (a∋gfImage cn) - be70 x ax ( case2 ncn ) = b∋g⁻¹ ax (nimg ax ncn) - - be71 : (x : Ordinal) (bx : odef (* b) x) → (or : CC1 x) → odef (* a) (h⁻¹ bx or ) - be71 x bx ( case1 cn ) = ? - be71 x bx ( case2 ncn ) = a∋fba x bx - - be71-1 : (x : Ordinal) (bx : odef (* b) x) - → (or : (odef ( Image (& UC) (Injection-⊆ UC⊆a f)) x)) - → gfImage (h⁻¹ bx (case1 ? ) ) - be71-1 x bx cn = ? -- subst₂ (λ j k → odef j k ) *iso refl (be08 (subst (λ k → odef k x) (sym *iso) cn)) - - be70-1 : (x : Ordinal) (lt : odef (* a) x) → (or : gfImage x ∨ (¬ gfImage x )) → odef ( Image (& UC) (Injection-⊆ UC⊆a f)) (h lt or ) - be70-1 = ? - - be74 : (x : Ordinal) (ax : odef (* a) x) (cc0 : CC0 x) → odef (* b) (h ax cc0 ) - be74 x ax with cc0 - ... | t = ? - - be75 : (x : Ordinal) (bx : odef (* b) x) → (cc1 : CC1 x) → odef (* a) (h⁻¹ bx cc1 ) - be75 x lt = ? - - fba-image : {x : Ordinal } → (bx : odef (* b) x) → odef (Image b g) (fba x bx) - fba-image {x} bx = record { y = _ ; ay = bx ; x=fy = refl } - - ImageUnique : {a b x : Ordinal } → {F : Injection a b} → (i j : odef (Image a F) x ) → IsImage.y i ≡ IsImage.y j - ImageUnique {a} {b} {x} {F} i j = inject F _ _ (IsImage.ay i) (IsImage.ay j) (trans (sym (IsImage.x=fy i)) (IsImage.x=fy j)) - - be72 : (x : Ordinal) (bx : odef (* b) x) → (cc1 : CC1 x ) → h (be75 x bx cc1) (cc0 (h⁻¹ bx cc1)) ≡ x - be72 x bx (case1 x₁) = ? - be72 x bx (case2 x₁) = ? - - - be73 : (x : Ordinal) (ax : odef (* a) x) → (cc0 : CC0 x ) → h⁻¹ (be74 x ax cc0) (cc1 (h ax cc0)) ≡ x - be73 x ax (case1 x₁) = ? - be73 x ax (case2 x₁) = ? - _c<_ : ( A B : HOD ) → Set n A c< B = ¬ ( Injection (& A) (& B) )