Mercurial > hg > Members > kono > Proof > ZF-in-agda

changeset 1457:79cf38cc667b

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 08 Jul 2023 08:56:01 +0900
parents ecfc24f53df4
children 171c3f3cdc6b
files src/Tychonoff.agda src/cardinal.agda
diffstat 2 files changed, 82 insertions(+), 80 deletions(-) [+]
line wrap: on
line diff
--- a/src/Tychonoff.agda	Fri Jul 07 17:37:04 2023 +0900
+++ b/src/Tychonoff.agda	Sat Jul 08 08:56:01 2023 +0900
@@ -35,7 +35,6 @@
 open import filter-util O
 open import ZProduct O
 open import Topology O
-open import maximum-filter O
 
 open Filter
 open Topology
@@ -189,13 +188,22 @@
      -- then we have maximum ultra filter ( Zorn lemma )
      --    to debug this file, commet out the maximum filter and open import
      --    otherwise the check requires a minute
+     --    but to check the proof, we have to connect it
      --
-     maxf : {X : Ordinal} → o∅ o< X → (CSX : * X ⊆ CS TP) → (fp : fip {X} CSX) → MaximumFilter (λ x → x) (F CSX fp)
-     maxf {X} 0<X CSX fp = F→Maximum {Power P} {P} (λ x → x) (CAP P)  (F CSX fp) 0<PP (N∋nc 0<X CSX fp) (proper CSX fp)
-     mf : {X : Ordinal} → o∅ o< X → (CSX : * X ⊆ CS TP) → (fp : fip {X} CSX) → Filter {Power P} {P} (λ x → x)
-     mf {X} 0<X CSX fp =  ? -- MaximumFilter.mf (maxf 0<X CSX fp)
-     ultraf : {X : Ordinal} → (0<X : o∅ o< X ) → (CSX : * X ⊆ CS TP) → (fp : fip {X} CSX) → ultra-filter ( mf 0<X CSX fp)
-     ultraf {X} 0<X CSX fp = F→ultra {Power P} {P} (λ x → x) (CAP P) (F CSX fp)  0<PP (N∋nc 0<X CSX fp) (proper CSX fp)
+     -- open import maximum-filter O
+     -- maxf : {X : Ordinal} → o∅ o< X → (CSX : * X ⊆ CS TP) → (fp : fip {X} CSX) → MaximumFilter (λ x → x) (F CSX fp)
+     -- maxf {X} 0<X CSX fp = F→Maximum {Power P} {P} (λ x → x) (CAP P)  (F CSX fp) 0<PP (N∋nc 0<X CSX fp) (proper CSX fp)
+     -- mf : {X : Ordinal} → o∅ o< X → (CSX : * X ⊆ CS TP) → (fp : fip {X} CSX) → Filter {Power P} {P} (λ x → x)
+     -- mf {X} 0<X CSX fp =  MaximumFilter.mf (maxf 0<X CSX fp)
+     -- ultraf : {X : Ordinal} → (0<X : o∅ o< X ) → (CSX : * X ⊆ CS TP) → (fp : fip {X} CSX) → ultra-filter ( mf 0<X CSX fp)
+     -- ultraf {X} 0<X CSX fp = F→ultra {Power P} {P} (λ x → x) (CAP P) (F CSX fp)  0<PP (N∋nc 0<X CSX fp) (proper CSX fp)
+
+     postulate 
+        maxf   : {X : Ordinal} → o∅ o< X → (CSX : * X ⊆ CS TP) → (fp : fip {X} CSX) → MaximumFilter (λ x → x) (F CSX fp)
+     mf     : {X : Ordinal} → o∅ o< X → (CSX : * X ⊆ CS TP) → (fp : fip {X} CSX) → Filter {Power P} {P} (λ x → x)
+     mf {X} 0<X CSX fp =  MaximumFilter.mf (maxf 0<X CSX fp)
+     postulate 
+        ultraf : {X : Ordinal} → (0<X : o∅ o< X ) → (CSX : * X ⊆ CS TP) → (fp : fip {X} CSX) → ultra-filter ( mf 0<X CSX fp)
      --
      -- so it has a limit as a limit of FIP
      --
@@ -237,11 +245,14 @@
         uf05 : odef (filter (MaximumFilter.mf (maxf 0<X CSX fp))) x
         uf05 = MaximumFilter.F⊆mf (maxf 0<X CSX fp) record { b = & (* x , * x) ; b⊆X = uf07
            ; sb = gi (subst (λ k → odef k x) (sym *iso) (case1 (sym &iso)) )  ; u⊆P = x⊆P ; x⊆u = λ x → x  }
-        uf061 : odef (filter (MaximumFilter.mf (maxf 0<X CSX fp))) (& (* (& (P ＼ * x ))))
-        uf061 = UFLP.is-limit ( uflp (mf 0<X CSX fp) (ultraf 0<X CSX fp)) {& (P ＼ * x)} uf03
+        -- if we postulate maximum filter, uf061 is an error
+        -- uf061 : odef (filter (MaximumFilter.mf (maxf 0<X CSX fp))) (& (* (& (P ＼ * x ))))
+        -- uf061 = UFLP.is-limit ( uflp (mf 0<X CSX fp) (ultraf 0<X CSX fp)) {& (P ＼ * x)} uf03
         -- uf06 (same as uf061) have yellow if zorn lemma is not imported
+        uf063 : odef (filter (mf 0<X CSX fp)) (& (* (& (P ＼ * x))))
+        uf063 = UFLP.is-limit ( uflp (mf 0<X CSX fp) (ultraf 0<X CSX fp)) {& (P ＼ * x)} uf03  
         uf06 : odef (filter (MaximumFilter.mf (maxf 0<X CSX fp))) (& (P ＼ * x ))
-        uf06 = subst (λ k → odef (filter (MaximumFilter.mf (maxf 0<X CSX fp))) k) &iso (UFLP.is-limit ( uflp (mf 0<X CSX fp) (ultraf 0<X CSX fp)) {& (P ＼ * x)} uf03  )
+        uf06 = subst (λ k → odef (filter (MaximumFilter.mf (maxf 0<X CSX fp))) k) &iso uf063
         uf13 : & ((* x) ∩ (P ＼ * x )) ≡ o∅
         uf13 = subst₂ (λ j k → j ≡ k ) refl ord-od∅ (cong (&) ( ==→o≡ record { eq→ = uf14 ; eq← = λ {x} lt → ⊥-elim (¬x<0 lt) }  ) ) where
            uf14 : {y : Ordinal} → odef (* x ∩ (P ＼ * x)) y → odef od∅ y
@@ -367,18 +378,6 @@
 postulate f-extensionality : { n m : Level}  → Axiom.Extensionality.Propositional.Extensionality n m
 open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ )
 
---    FilterQP : {P Q : HOD } → (F : Filter {Power (ZFP P Q)} {ZFP P Q} (λ x → x))  
---         → Filter {Power (ZFP Q P)} {ZFP Q P} (λ x → x) 
---    FilterQP {P} {Q} F = record { filter = ? ; f⊆L = ? ; filter1 = ? ; filter2 = ? } 
--- 
---    projection-of-filter : {P Q : HOD } → (F : Filter {Power (ZFP P Q)} {ZFP P Q} (λ x → x))  
---         → Filter {Power P} {P} (λ x → x) 
---    projection-of-filter = ?
--- 
---    projection-of-ultra-filter : {P Q : HOD } → (F : Filter {Power (ZFP P Q)} {ZFP P Q} (λ x → x))  (UF : ultra-filter F) 
---         → ultra-filter (projection-of-filter F)
---    projection-of-ultra-filter = ?
-
 --
 -- We have UFLP both in P and Q. Given an ultra filter F on P x Q. It has limits on P and Q because a projection of ultra filter
 -- is a ultra filter. Show the product of the limits is a limit of P x Q. A neighbor of P x Q contains subbase of P x Q,
--- a/src/cardinal.agda	Fri Jul 07 17:37:04 2023 +0900
+++ b/src/cardinal.agda	Sat Jul 08 08:56:01 2023 +0900
@@ -133,27 +133,28 @@
 --  f : A → B        OrdBijection A           (Image A f)
 --  g : B → A        OrdBijection (Image B g) B
 --                     UC (closure of g ∙ f from ¬ Image B g )
---                         A =   UC ∪ (A \ Image B g )
+--                         A =   UC ∪ (A \ Image B gi )
 --                         B =   (Image B g) UC 
 --
 Bernstein : {a b : Ordinal } → Injection a b → Injection b a → HODBijection (* a) (* b)
-Bernstein {a} {b} (f @ record { i→ = fab ; iB = b∋fab ; inject = fab-inject }) ( g @ record { i→ = fba ; iB = a∋fba ; inject = fba-inject })
+Bernstein {a} {b} ( fi @ record { i→ = f ; iB = b∋f ; inject = f-inject }) 
+                  ( gi @ record { i→ = g ; iB = a∋g ; inject = g-inject })
      = subst₂ (λ j k → HODBijection j k ) (sym a=UC∨a-UC) (sym b=fUC∨b-fUC) (bi-∪  bi-UC  bi-fUC)
  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) } 
+      gf = record { i→ = λ x ax → g (f x ax) (b∋f x ax) ; iB = λ x ax → a∋g _ (b∋f x ax) 
+         ; inject = λ x y ax ay eq → f-inject _ _ ax ay ( g-inject _ _ (b∋f _ ax) (b∋f _ ay) eq) } 
 
       --
-      -- HOD UC is closure of g ∙ f starting from a - Image g
+      -- HOD UC is closure of gi ∙ fi starting from a - Image g
       --
       data gfImage :  (x : Ordinal) → Set n where
-          a-g : {x : Ordinal} → (ax : odef (* a) x ) → (¬ib : ¬ ( IsImage b a g x )) → gfImage  x
+          a-g : {x : Ordinal} → (ax : odef (* a) x ) → (¬ib : ¬ ( IsImage b a gi x )) → gfImage  x
           next-gf : {x : Ordinal} → (ix : IsImage a a gf x) → (gfiy : gfImage (IsImage0.y ix) ) → gfImage  x
 
       a∋gfImage : {x : Ordinal } → gfImage x → odef (* a) x
       a∋gfImage {x} (a-g ax ¬ib) = ax
-      a∋gfImage  {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) )
+      a∋gfImage  {x} (next-gf record { y = y ; ay = ay ; x=fy = x=fy } lt ) = subst (λ k → odef (* a) k ) (sym x=fy) (a∋g _ (b∋f y ay) )
 
       UC : HOD
       UC = record { od = record { def = λ x → gfImage x } ; odmax = & (* a) ; <odmax = λ lt → odef< (a∋gfImage lt)  }
@@ -173,13 +174,13 @@
            be01 {x} (case2 ngfx) = proj1 ngfx
 
       FA : (x : Ordinal) → (ax : gfImage x) → Ordinal
-      FA x ax = fab x (a∋gfImage ax)
+      FA x ax = f 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))
+      b∋f⁻¹ : (x : Ordinal) → IsImage0 UC (* b) FA x → odef (* b) x
+      b∋f⁻¹ x record { y = y ; ay = ay ; x=fy = x=fy } = subst (λ k → odef (* b) k ) (sym x=fy) (b∋f y (a∋gfImage ay))
 
       fUC : HOD
-      fUC = record { od = record { def = λ x → IsImage0 UC (* b) FA  x } ; odmax = & (* b) ; <odmax = λ {x} lt → odef< (b∋Uf1 x lt)} 
+      fUC = record { od = record { def = λ x → IsImage0 UC (* b) FA  x } ; odmax = & (* b) ; <odmax = λ {x} lt → odef< (b∋f⁻¹ x lt)} 
 
       b-fUC : HOD
       b-fUC = record { od = record { def = λ x → odef (* b) x ∧ (¬ IsImage0 UC (* b) FA  x) } ; odmax = & (* b) ; <odmax = λ lt → odef∧< lt  }
@@ -191,69 +192,69 @@
            ... | case1 gfx = case1 gfx
            ... | case2 ngfx = case2 ⟪ bx , ngfx ⟫
            be01 : {x : Ordinal} → odef (fUC ∪ b-fUC) x → odef (* b) x 
-           be01 {x} (case1 record { y = y ; ay = ay ; x=fy = x=fy }) = subst (λ k → odef (* b) k) (sym x=fy) ( b∋fab y (a∋gfImage ay))
+           be01 {x} (case1 record { y = y ; ay = ay ; x=fy = x=fy }) = subst (λ k → odef (* b) k) (sym x=fy) ( b∋f y (a∋gfImage ay))
            be01 {x} (case2 ngfx) = proj1 ngfx
 
-      nimg : {x : Ordinal } → (ax : odef (* a) x ) → ¬ (odef UC x) → IsImage b a g x
-      nimg {x} ax ncn with ODC.p∨¬p O (IsImage b a g x)
+      nimg : {x : Ordinal } → (ax : odef (* a) x ) → ¬ (odef UC x) → IsImage b a gi x
+      nimg {x} ax ncn with ODC.p∨¬p O (IsImage b a gi x)
       ... | case1 img = img
       ... | case2 nimg = ⊥-elim ( ncn (a-g ax nimg ) )
 
-      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 ))  
+      f-cong : {x y : Ordinal } → {ax : odef (* a) x} {ax1 : odef (* a) y}  → x ≡ y  → f x ax ≡ f y ax1
+      f-cong {x} {x} {ax} {ax1} refl = cong (λ k → f 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 ))  
+      g-cong : {x y : Ordinal } → {bx : odef (* b) x} {bx1 : odef (* b) y}  → x ≡ y  → g x bx ≡ g y bx1
+      g-cong {x} {x} {bx} {bx1} refl = cong (λ k → g x k) ( HE.≅-to-≡ ( ∋-irr {* b} bx bx1 ))  
 
-      g⁻¹ : {x : Ordinal } → (ax : odef (* a) x) → (nc0 : IsImage b a g x ) → Ordinal
+      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
 
-      b∋g⁻¹ : {x : Ordinal } → (ax : odef (* a) x) (nc0 : IsImage b a g x ) → odef (* b) (g⁻¹ ax nc0)
+      b∋g⁻¹ : {x : Ordinal } → (ax : odef (* a) x) (nc0 : IsImage b a gi x ) → odef (* b) (g⁻¹ ax nc0)
       b∋g⁻¹ {x} ax record { y = y ; ay = ay ; x=fy = x=fy } = ay
 
-      g⁻¹-iso : {x : Ordinal } → (ax : odef (* a) x) → (nc0 : IsImage b a g x ) → fba (g⁻¹ ax nc0) (b∋g⁻¹ ax nc0) ≡ x
+      g⁻¹-iso : {x : Ordinal } → (ax : odef (* a) x) → (nc0 : IsImage b a gi x ) → g (g⁻¹ ax nc0) (b∋g⁻¹ ax nc0) ≡ x
       g⁻¹-iso {x} ax record { y = y ; ay = ay ; x=fy = x=fy } = sym x=fy
 
-      g⁻¹-iso1 : {x : Ordinal } → (bx : odef (* b) x) → (nc0 : IsImage b a g (fba x bx) )  → g⁻¹ (a∋fba x bx) nc0  ≡ x
-      g⁻¹-iso1 {x} bx nc0 = inject g _ _ (b∋g⁻¹ (a∋fba x bx) nc0) bx (g⁻¹-iso (a∋fba x bx) nc0) 
+      g⁻¹-iso1 : {x : Ordinal } → (bx : odef (* b) x) → (nc0 : IsImage b a gi (g x bx) )  → g⁻¹ (a∋g x bx) nc0  ≡ x
+      g⁻¹-iso1 {x} bx nc0 = inject gi _ _ (b∋g⁻¹ (a∋g x bx) nc0) bx (g⁻¹-iso (a∋g x bx) nc0) 
 
-      g⁻¹-eq : {x : Ordinal } → (ax ax' : odef (* a) x) → {nc0 nc0' : IsImage b a g x } → g⁻¹ ax nc0 ≡ g⁻¹ ax' nc0'
+      g⁻¹-eq : {x : Ordinal } → (ax ax' : odef (* a) x) → {nc0 nc0' : IsImage b a gi x } → g⁻¹ ax nc0 ≡ g⁻¹ ax' nc0'
       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 )
+           = inject gi _ _ ay₁ ay (trans (sym x=fy₁) x=fy )
 
       cc11-case2 : {x : Ordinal} (ax : odef (* a) x) 
           → (ncn : ¬ gfImage x) 
-          → ¬ IsImage0 UC (* b) (λ x ax → fab x (a∋gfImage ax))  (g⁻¹ ax (nimg ax ncn))
+          → ¬ IsImage0 UC (* b) (λ x ax → f x (a∋gfImage ax))  (g⁻¹ ax (nimg ax ncn))
       cc11-case2 {x} ax ncn record { y = y ; ay = ay ; x=fy = x=fy } with nimg ax ncn
       ... | record { y = y1 ; ay = ay1 ; x=fy = x=fy1 } = ncn ( subst (λ k → gfImage k) be113 
                                             (next-gf record { y = y ; ay = (a∋gfImage ay) ; x=fy = refl } ay ) )  where
-               be113 : fba (fab y (a∋gfImage ay)) (b∋fab y (a∋gfImage ay)) ≡ x
+               be113 : g (f y (a∋gfImage ay)) (b∋f y (a∋gfImage ay)) ≡ x
                be113 = begin
-                    fba (fab y (a∋gfImage ay)) (b∋fab y (a∋gfImage ay)) ≡⟨ fba-eq (sym x=fy)  ⟩
-                    fba y1 ay1 ≡⟨ sym (x=fy1) ⟩
+                    g (f y (a∋gfImage ay)) (b∋f y (a∋gfImage ay)) ≡⟨ g-cong (sym x=fy)  ⟩
+                    g y1 ay1 ≡⟨ sym (x=fy1) ⟩
                     x ∎ where open ≡-Reasoning
 
       cc10-case2 : {x : Ordinal } → (bx : odef (* b) x )
-         → ¬ IsImage0 UC (* b) (λ x ax → fab x (a∋gfImage ax))  x
-         → ¬ gfImage (fba x bx)
+         → ¬ IsImage0 UC (* b) (λ x ax → f x (a∋gfImage ax))  x
+         → ¬ gfImage (g x bx)
       cc10-case2 {x} bx nix (a-g ax ¬ib) = ¬ib record { y = _ ; ay = bx ; x=fy = refl }
       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))) }
+           = nix record { y = _ ; ay = gfy ; x=fy = inject gi _ _ bx (b∋f y (a∋gfImage gfy)) (trans x=fy (g-cong (f-cong refl))) }
 
       fU1 : (x : Ordinal) → odef UC x → Ordinal
-      fU1 x gfx = fab x (a∋gfImage gfx)
+      fU1 x gfx = f x (a∋gfImage gfx)
 
-      Uf1 : (x : Ordinal) → IsImage0 UC (* b) FA x → Ordinal
-      Uf1 x record { y = y ; ay = ay ; x=fy = x=fy } = y
+      f⁻¹ : (x : Ordinal) → IsImage0 UC (* b) FA x → Ordinal
+      f⁻¹ x record { y = y ; ay = ay ; x=fy = x=fy } = y
 
-      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
+      UC∋f⁻¹ : {x : Ordinal } → (lt : odef fUC x) → odef UC (f⁻¹ x lt )
+      UC∋f⁻¹ {x} record { y = y ; ay = ay ; x=fy = x=fy } = ay
 
-      fU-iso1 : {x : Ordinal } → (lt : odef fUC x) → fU1 (Uf1 x lt) (UC∋Uf1 lt) ≡ x
-      fU-iso1 {x} record { y = y ; ay = (a-g ax ¬ib) ; x=fy = x=fy } = trans (fab-eq refl) (sym x=fy) 
-      fU-iso1 {x} record { y = y ; ay = (next-gf record { y = y₁ ; ay = ay₁ ; x=fy = x=fy₁ } ay) ; x=fy = x=fy } = trans (fab-eq refl) (sym x=fy) 
+      fU-iso1 : {x : Ordinal } → (lt : odef fUC x) → fU1 (f⁻¹ x lt) (UC∋f⁻¹ lt) ≡ x
+      fU-iso1 {x} record { y = y ; ay = (a-g ax ¬ib) ; x=fy = x=fy } = trans (f-cong refl) (sym x=fy) 
+      fU-iso1 {x} record { y = y ; ay = (next-gf record { y = y₁ ; ay = ay₁ ; x=fy = x=fy₁ } ay) ; x=fy = x=fy } = trans (f-cong refl) (sym x=fy) 
 
-      fU-iso0 : {x : Ordinal } → (lt : odef UC x) → Uf1 (fU1 x lt) record { y = _ ; ay = lt ; x=fy = refl } ≡ x
+      fU-iso0 : {x : Ordinal } → (lt : odef UC x) → f⁻¹ (fU1 x lt) record { y = _ ; ay = lt ; x=fy = refl } ≡ x
       fU-iso0 {x} (a-g ax ¬ib) = refl 
       fU-iso0 {x} (next-gf record { y = y ; ay = ay ; x=fy = x=fy } lt) = refl
 
@@ -261,15 +262,15 @@
       -- We cannot directly create h : * a → * b , because the cnoise of UC ∨  a-UC is non constructive and
       -- even LEM cannot be used in positive context. The merging bi-UC and  bi-fUC uses also LEM but use it positively.
       --
-      -- bijection on each side is easy, because these are images of f and g.
+      -- bijection on each side is easy, because these are images of fi and g.
       --    somehow we don't use injection of f.
 
       bi-UC : HODBijection UC fUC
       bi-UC = record { 
-         fun→  = λ x lt → fU1 x lt
-       ; fun←  = λ x lt → Uf1 x lt
+         fun→  = λ x lt → f x (a∋gfImage lt)
+       ; fun←  = λ x lt → f⁻¹ x lt
        ; funB  = λ x lt → record { y = _ ; ay = lt  ; x=fy = refl }
-       ; funA  = λ x lt → UC∋Uf1 lt
+       ; funA  = λ x lt → UC∋f⁻¹ lt
        ; fiso→ = λ x lt → fU-iso1 lt
        ; fiso← = λ x lt → fU-iso0 lt
        }
@@ -277,21 +278,21 @@
       b-FUC∋g⁻¹ : {x : Ordinal } → (lt : odef a-UC x )→ odef b-fUC (g⁻¹ (proj1 lt) (nimg (proj1 lt) (proj2 lt))) 
       b-FUC∋g⁻¹ {x} ⟪ ax , ngfix ⟫ = ⟪ b∋g⁻¹ ax (nimg ax ngfix) , cc11-case2 ax ngfix  ⟫
 
-      a-UC∋g : {x : Ordinal } → (lt : odef b-fUC x) → odef a-UC (fba x (proj1 lt ))
-      a-UC∋g {x} ⟪ bx , ¬img ⟫ = ⟪ a∋fba x bx , cc10-case2 bx ¬img ⟫
+      a-UC∋g : {x : Ordinal } → (lt : odef b-fUC x) → odef a-UC (g x (proj1 lt ))
+      a-UC∋g {x} ⟪ bx , ¬img ⟫ = ⟪ a∋g x bx , cc10-case2 bx ¬img ⟫
 
       fUC-iso1 : {x : Ordinal } → (lt : odef b-fUC x ) → g⁻¹ (proj1 (a-UC∋g lt)) (nimg (proj1 (a-UC∋g lt)) (proj2 (a-UC∋g lt))) ≡ x
       fUC-iso1 {x} lt with nimg (proj1 (a-UC∋g lt)) (proj2 (a-UC∋g lt))
-      ... | record { y = y ; ay = ay ; x=fy = x=fy } = sym ( inject g _ _ (proj1 lt) ay x=fy )
+      ... | record { y = y ; ay = ay ; x=fy = x=fy } = sym ( inject gi _ _ (proj1 lt) ay x=fy )
 
-      fUC-iso0 : {x : Ordinal} → (lt : odef a-UC x) →  fba (g⁻¹ (proj1 lt) (nimg (proj1 lt) (proj2 lt))) (proj1 (b-FUC∋g⁻¹ lt)) ≡ x
+      fUC-iso0 : {x : Ordinal} → (lt : odef a-UC x) →  g (g⁻¹ (proj1 lt) (nimg (proj1 lt) (proj2 lt))) (proj1 (b-FUC∋g⁻¹ lt)) ≡ x
       fUC-iso0 {x} lt with nimg (proj1 lt) (proj2 lt)
       ... | record { y = y ; ay = ay ; x=fy = x=fy } = sym x=fy
 
       bi-fUC : HODBijection a-UC b-fUC
       bi-fUC = record { 
          fun→  = λ x lt → g⁻¹ (proj1 lt) (nimg (proj1 lt) (proj2 lt))
-       ; fun←  = λ x lt → fba x (proj1 lt)
+       ; fun←  = λ x lt → g x (proj1 lt)
        ; funB  = λ x lt → b-FUC∋g⁻¹  lt
        ; funA  = λ x lt → a-UC∋g lt
        ; fiso→ = λ x lt → fUC-iso1 lt
@@ -325,13 +326,13 @@
 ... | case1 a = true
 ... | case2 b = false
 
-fun←eq : {P S : HOD} (b : HODBijection P S ) {x y : Ordinal } → {ax : odef S x} {ax1 : odef S y}  
+fun←cong : {P S : HOD} (b : HODBijection P S ) {x y : Ordinal } → {ax : odef S x} {ax1 : odef S y}  
     → x ≡ y  → fun← b x ax ≡ fun← b y ax1
-fun←eq {P} {S} b {x} {x} {ax} {ax1} refl = cong (λ k → fun← b x k) ( HE.≅-to-≡ ( ∋-irr {S} ax ax1 ))  
+fun←cong {P} {S} b {x} {x} {ax} {ax1} refl = cong (λ k → fun← b x k) ( HE.≅-to-≡ ( ∋-irr {S} ax ax1 ))  
      
-fun→eq : {P S : HOD} (b : HODBijection P S ) {x y : Ordinal } → {ax : odef P x} {ax1 : odef P y}  
+fun→cong : {P S : HOD} (b : HODBijection P S ) {x y : Ordinal } → {ax : odef P x} {ax1 : odef P y}  
     → x ≡ y  → fun→ b x ax ≡ fun→ b y ax1
-fun→eq {P} {S} b {x} {x} {ax} {ax1} refl = cong (λ k → fun→ b x k) ( HE.≅-to-≡ ( ∋-irr {P} ax ax1 ))  
+fun→cong {P} {S} b {x} {x} {ax} {ax1} refl = cong (λ k → fun→ b x k) ( HE.≅-to-≡ ( ∋-irr {P} ax ax1 ))  
      
 
 --    S
@@ -355,8 +356,10 @@
              c01 y (case2 eq) = subst₂ (λ j k  → odef j k ) *iso (trans (sym &iso) (sym eq) ) lt
      f2 : Injection (& (Power S)) (& S) 
      f2 = f
-     b : HODBijection (Power S) S 
-     b = subst₂ (λ j k → HODBijection j k) *iso *iso ( Bernstein f2 f1)   -- this makes check very slow
+     postulate 
+         b : HODBijection (Power S) S 
+     -- b = subst₂ (λ j k → HODBijection j k) *iso *iso ( 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∅
      --
@@ -401,7 +404,7 @@
           not (is-S (* (& Diag)) n)
         ≡⟨ cong (λ k → not (is-S (* k) n)) (sym (fiso← b (& Diag) diag3 )) ⟩
           not (  is-S (* (fun← b (fun→ b (& Diag) diag3) (funB b (& Diag) diag3 ))) n ) 
-        ≡⟨ cong (λ k → not (is-S (* k) n)) ( fun←eq b {_} {_} {funB b _ diag3} {sn} dn )   ⟩
+        ≡⟨ cong (λ k → not (is-S (* k) n)) ( fun←cong b {_} {_} {funB b _ diag3} {sn} dn )   ⟩
           not (  is-S (* (fun← b n sn )) n ) 
         ≡⟨ not-isD _ sn  ⟩
           is-S Diag n
@@ -419,7 +422,7 @@
             → fun← ceq x (subst (λ k → odef k x) *iso ltx) ≡ fun← ceq y (subst (λ k → odef k y) *iso lty) → x ≡ y
          c04 x y ltx lty eq = begin
            x ≡⟨ sym ( fiso→ ceq x c05 ) ⟩
-           fun→ ceq ( fun← ceq x c05 ) (funA ceq x c05)  ≡⟨ fun←eq (hodbij-sym ceq) eq ⟩
+           fun→ ceq ( fun← ceq x c05 ) (funA ceq x c05)  ≡⟨ fun←cong (hodbij-sym ceq) eq ⟩
            fun→ ceq ( fun← ceq y c06 ) (funA ceq y c06)  ≡⟨ fiso→ ceq y c06 ⟩
            y ∎ where 
              open ≡-Reasoning