# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1596247589 -32400
# Node ID 44a484f17f26a6ad382cb6c51fe20ca98665ae2a
# Parent  cb067605fea09c34eda9a48e79e25cb9477b1edc
syntax *, &,  ⟪ , ⟫

diff -r cb067605fea0 -r 44a484f17f26 BAlgbra.agda
--- a/BAlgbra.agda	Fri Jul 31 17:54:52 2020 +0900
+++ b/BAlgbra.agda	Sat Aug 01 11:06:29 2020 +0900
@@ -13,7 +13,7 @@
 open import Relation.Binary
 open import Relation.Binary.Core
 open import  Relation.Binary.PropositionalEquality
-open import Data.Nat renaming ( zero to Zero ; suc to Suc ;  ℕ to Nat ; _⊔_ to _n⊔_ ) 
+open import Data.Nat renaming ( zero to Zero ; suc to Suc ;  ℕ to Nat ; _⊔_ to _n⊔_ ; _+_ to _n+_ )  
 
 open inOrdinal O
 open OD O
@@ -43,73 +43,72 @@
 ∪-Union {A} {B} = ==→o≡ ( record { eq→ =  lemma1 ; eq← = lemma2 } )  where
     lemma1 :  {x : Ordinal} → odef (Union (A , B)) x → odef (A ∪ B) x
     lemma1 {x} lt = lemma3 lt where
-        lemma4 : {y : Ordinal} → odef (A , B) y ∧ odef (ord→od y) x → ¬ (¬ ( odef A x ∨ odef B x) )
+        lemma4 : {y : Ordinal} → odef (A , B) y ∧ odef (* y) x → ¬ (¬ ( odef A x ∨ odef B x) )
         lemma4 {y} z with proj1 z
-        lemma4 {y} z | case1 refl = double-neg (case1 ( subst (λ k → odef k x ) oiso (proj2 z)) )
-        lemma4 {y} z | case2 refl = double-neg (case2 ( subst (λ k → odef k x ) oiso (proj2 z)) )
-        lemma3 : (((u : Ordinals.ord O) → ¬ odef (A , B) u ∧ odef (ord→od u) x) → ⊥) → odef (A ∪ B) x
+        lemma4 {y} z | case1 refl = double-neg (case1 ( subst (λ k → odef k x ) *iso (proj2 z)) )
+        lemma4 {y} z | case2 refl = double-neg (case2 ( subst (λ k → odef k x ) *iso (proj2 z)) )
+        lemma3 : (((u : Ordinals.ord O) → ¬ odef (A , B) u ∧ odef (* u) x) → ⊥) → odef (A ∪ B) x
         lemma3 not = ODC.double-neg-eilm O (FExists _ lemma4 not)   -- choice
     lemma2 :  {x : Ordinal} → odef (A ∪ B) x → odef (Union (A , B)) x
-    lemma2 {x} (case1 A∋x) = subst (λ k → odef (Union (A , B)) k) diso ( IsZF.union→ isZF (A , B) (ord→od x) A
-       (record { proj1 = case1 refl ; proj2 = d→∋ A A∋x } ))
-    lemma2 {x} (case2 B∋x) = subst (λ k → odef (Union (A , B)) k) diso ( IsZF.union→ isZF (A , B) (ord→od x) B
-       (record { proj1 = case2 refl ; proj2 = d→∋ B B∋x } ))
+    lemma2 {x} (case1 A∋x) = subst (λ k → odef (Union (A , B)) k) &iso ( IsZF.union→ isZF (A , B) (* x) A
+        ⟪ case1 refl , d→∋ A A∋x ⟫ )
+    lemma2 {x} (case2 B∋x) = subst (λ k → odef (Union (A , B)) k) &iso ( IsZF.union→ isZF (A , B) (* x) B
+        ⟪ case2 refl , d→∋ B B∋x ⟫ )
 
 ∩-Select : { A B : HOD } →  Select A (  λ x → ( A ∋ x ) ∧ ( B ∋ x )  ) ≡ ( A ∩ B )
 ∩-Select {A} {B} = ==→o≡ ( record { eq→ =  lemma1 ; eq← = lemma2 } ) where
     lemma1 : {x : Ordinal} → odef (Select A (λ x₁ → (A ∋ x₁) ∧ (B ∋ x₁))) x → odef (A ∩ B) x
-    lemma1 {x} lt = record { proj1 = proj1 lt ; proj2 = subst (λ k → odef B k ) diso (proj2 (proj2 lt)) }
+    lemma1 {x} lt = ⟪ proj1 lt , subst (λ k → odef B k ) &iso (proj2 (proj2 lt)) ⟫
     lemma2 : {x : Ordinal} → odef (A ∩ B) x → odef (Select A (λ x₁ → (A ∋ x₁) ∧ (B ∋ x₁))) x
-    lemma2 {x} lt = record { proj1 = proj1 lt ; proj2 =
-        record { proj1 = d→∋ A (proj1 lt) ; proj2 = d→∋ B (proj2 lt) } }
+    lemma2 {x} lt = ⟪ proj1 lt , ⟪ d→∋ A (proj1 lt) , d→∋ B (proj2 lt) ⟫ ⟫
 
 dist-ord : {p q r : HOD } → p ∩ ( q ∪ r ) ≡   ( p ∩ q ) ∪ ( p ∩ r )
 dist-ord {p} {q} {r} = ==→o≡ ( record { eq→ = lemma1 ; eq← = lemma2 } ) where
     lemma1 :  {x : Ordinal} → odef (p ∩ (q ∪ r)) x → odef ((p ∩ q) ∪ (p ∩ r)) x
     lemma1 {x} lt with proj2 lt
-    lemma1 {x} lt | case1 q∋x = case1 ( record { proj1 = proj1 lt ; proj2 = q∋x } )
-    lemma1 {x} lt | case2 r∋x = case2 ( record { proj1 = proj1 lt ; proj2 = r∋x } )
+    lemma1 {x} lt | case1 q∋x = case1 ⟪ proj1 lt , q∋x ⟫ 
+    lemma1 {x} lt | case2 r∋x = case2 ⟪ proj1 lt , r∋x ⟫ 
     lemma2  : {x : Ordinal} → odef ((p ∩ q) ∪ (p ∩ r)) x → odef (p ∩ (q ∪ r)) x
-    lemma2 {x} (case1 p∩q) = record { proj1 = proj1 p∩q ; proj2 = case1 (proj2 p∩q ) } 
-    lemma2 {x} (case2 p∩r) = record { proj1 = proj1 p∩r ; proj2 = case2 (proj2 p∩r ) } 
+    lemma2 {x} (case1 p∩q) = ⟪ proj1 p∩q , case1 (proj2 p∩q ) ⟫ 
+    lemma2 {x} (case2 p∩r) = ⟪ proj1 p∩r , case2 (proj2 p∩r ) ⟫ 
 
 dist-ord2 : {p q r : HOD } → p ∪ ( q ∩ r ) ≡   ( p ∪ q ) ∩ ( p ∪ r )
 dist-ord2 {p} {q} {r} = ==→o≡ ( record { eq→ = lemma1 ; eq← = lemma2 } ) where
     lemma1 : {x : Ordinal} → odef (p ∪ (q ∩ r)) x → odef ((p ∪ q) ∩ (p ∪ r)) x
-    lemma1 {x} (case1 cp) = record { proj1 = case1 cp ; proj2 = case1 cp }
-    lemma1 {x} (case2 cqr) = record { proj1 = case2 (proj1 cqr) ; proj2 = case2 (proj2 cqr) }
+    lemma1 {x} (case1 cp) = ⟪ case1 cp , case1 cp ⟫
+    lemma1 {x} (case2 cqr) = ⟪ case2 (proj1 cqr) , case2 (proj2 cqr) ⟫
     lemma2 : {x : Ordinal} → odef ((p ∪ q) ∩ (p ∪ r)) x → odef (p ∪ (q ∩ r)) x
     lemma2 {x} lt with proj1 lt | proj2 lt
     lemma2 {x} lt | case1 cp | _ = case1 cp
     lemma2 {x} lt | _ | case1 cp = case1 cp 
-    lemma2 {x} lt | case2 cq | case2 cr = case2 ( record { proj1 = cq ; proj2 = cr } )
+    lemma2 {x} lt | case2 cq | case2 cr = case2 ⟪ cq , cr ⟫ 
 
 record IsBooleanAlgebra ( L : Set n)
        ( b1 : L )
        ( b0 : L )
        ( -_ : L → L  )
        ( _+_ : L → L → L )
-       ( _*_ : L → L → L ) : Set (suc n) where
+       ( _x_ : L → L → L ) : Set (suc n) where
    field
        +-assoc : {a b c : L } → a + ( b + c ) ≡ (a + b) + c
-       *-assoc : {a b c : L } → a * ( b * c ) ≡ (a * b) * c
+       x-assoc : {a b c : L } → a x ( b x c ) ≡ (a x b) x c
        +-sym : {a b : L } → a + b ≡ b + a
-       -sym : {a b : L } → a * b  ≡ b * a
-       -aab : {a b : L } → a + ( a * b ) ≡ a
-       *-aab : {a b : L } → a * ( a + b ) ≡ a
-       -dist : {a b c : L } → a + ( b * c ) ≡ ( a * b ) + ( a * c )
-       *-dist : {a b c : L } → a * ( b + c ) ≡ ( a + b ) * ( a + c )
+       -sym : {a b : L } → a x b  ≡ b x a
+       -aab : {a b : L } → a + ( a x b ) ≡ a
+       x-aab : {a b : L } → a x ( a + b ) ≡ a
+       -dist : {a b c : L } → a + ( b x c ) ≡ ( a x b ) + ( a x c )
+       x-dist : {a b c : L } → a x ( b + c ) ≡ ( a + b ) x ( a + c )
        a+0 : {a : L } → a + b0 ≡ a
-       a*1 : {a : L } → a * b1 ≡ a
+       ax1 : {a : L } → a x b1 ≡ a
        a+-a1 : {a : L } → a + ( - a ) ≡ b1
-       a*-a0 : {a : L } → a * ( - a ) ≡ b0
+       ax-a0 : {a : L } → a x ( - a ) ≡ b0
 
 record BooleanAlgebra ( L : Set n) : Set (suc n) where
    field
        b1 : L
        b0 : L
        -_ : L → L 
-       _++_ : L → L → L
-       _**_ : L → L → L
-       isBooleanAlgebra : IsBooleanAlgebra L b1 b0 -_ _++_ _**_
+       _+_ : L → L → L
+       _x_ : L → L → L
+       isBooleanAlgebra : IsBooleanAlgebra L b1 b0 -_ _+_ _x_
        
diff -r cb067605fea0 -r 44a484f17f26 LEMC.agda
--- a/LEMC.agda	Fri Jul 31 17:54:52 2020 +0900
+++ b/LEMC.agda	Sat Aug 01 11:06:29 2020 +0900
@@ -52,18 +52,18 @@
 record choiced  ( X : Ordinal ) : Set n where
   field
      a-choice : Ordinal
-     is-in : odef (ord→od X) a-choice
+     is-in : odef (* X) a-choice
 
 open choiced
 
--- ∋→d : ( a : HOD  ) { x : HOD } → ord→od (od→ord a) ∋ x → X ∋ ord→od (a-choice (choice-func X not))
--- ∋→d a lt = subst₂ (λ j k → odef j k) oiso (sym diso) lt
+-- ∋→d : ( a : HOD  ) { x : HOD } → * (& a) ∋ x → X ∋ * (a-choice (choice-func X not))
+-- ∋→d a lt = subst₂ (λ j k → odef j k) *iso (sym &iso) lt
 
-oo∋ : { a : HOD} {  x : Ordinal } → odef (ord→od (od→ord a)) x → a ∋ ord→od x
-oo∋ lt = subst₂ (λ j k → odef j k) oiso (sym diso) lt
+oo∋ : { a : HOD} {  x : Ordinal } → odef (* (& a)) x → a ∋ * x
+oo∋ lt = subst₂ (λ j k → odef j k) *iso (sym &iso) lt
 
-∋oo : { a : HOD} {  x : Ordinal } → a ∋ ord→od x → odef (ord→od (od→ord a)) x 
-∋oo lt = subst₂ (λ j k → odef j k ) (sym oiso) diso lt 
+∋oo : { a : HOD} {  x : Ordinal } → a ∋ * x → odef (* (& a)) x 
+∋oo lt = subst₂ (λ j k → odef j k ) (sym *iso) &iso lt 
 
 OD→ZFC : ZFC
 OD→ZFC   = record { 
@@ -78,22 +78,18 @@
     -- infixr  230 _∩_ _∪_
     isZFC : IsZFC (HOD )  _∋_  _=h=_ od∅ Select
     isZFC = record {
-       choice-func = λ A {X} not A∋X → ord→od (a-choice (choice-func X not) );
+       choice-func = λ A {X} not A∋X → * (a-choice (choice-func X not) );
        choice = λ A {X} A∋X not → oo∋ (is-in (choice-func X not))
      } where
          --
          -- the axiom choice from LEM and OD ordering
          --
-         choice-func :  (X : HOD ) → ¬ ( X =h= od∅ ) → choiced (od→ord X)
+         choice-func :  (X : HOD ) → ¬ ( X =h= od∅ ) → choiced (& X)
          choice-func  X not = have_to_find where
                  ψ : ( ox : Ordinal ) → Set n
-                 ψ ox = (( x : Ordinal ) → x o< ox  → ( ¬ odef X x )) ∨ choiced (od→ord X)
+                 ψ ox = (( x : Ordinal ) → x o< ox  → ( ¬ odef X x )) ∨ choiced (& X)
                  lemma-ord : ( ox : Ordinal  ) → ψ ox
                  lemma-ord  ox = TransFinite {ψ} induction ox where
-                    -- ∋-p : (A x : HOD ) → Dec ( A ∋ x ) 
-                    -- ∋-p A x with p∨¬p (Lift (suc n) ( A ∋ x )) -- LEM
-                    -- ∋-p A x | case1 (lift t)  = yes t
-                    -- ∋-p A x | case2 t  = no (λ x → t (lift x ))
                     ∀-imply-or :  {A : Ordinal  → Set n } {B : Set n }
                         → ((x : Ordinal ) → A x ∨ B) →  ((x : Ordinal ) → A x) ∨ B
                     ∀-imply-or  {A} {B} ∀AB with p∨¬p ((x : Ordinal ) → A x) -- LEM
@@ -104,18 +100,18 @@
                          lemma not | case1 b = b
                          lemma not | case2 ¬b = ⊥-elim  (not (λ x → dont-orb (∀AB x) ¬b ))
                     induction : (x : Ordinal) → ((y : Ordinal) → y o< x → ψ y) → ψ x
-                    induction x prev with ∋-p X ( ord→od x) 
+                    induction x prev with ∋-p X ( * x) 
                     ... | yes p = case2 ( record { a-choice = x ; is-in = ∋oo  p } )
                     ... | no ¬p = lemma where
-                         lemma1 : (y : Ordinal) → (y o< x → odef X y → ⊥) ∨ choiced (od→ord X)
-                         lemma1 y with ∋-p X (ord→od y)
+                         lemma1 : (y : Ordinal) → (y o< x → odef X y → ⊥) ∨ choiced (& X)
+                         lemma1 y with ∋-p X (* y)
                          lemma1 y | yes y<X = case2 ( record { a-choice = y ; is-in = ∋oo y<X } )
                          lemma1 y | no ¬y<X = case1 ( λ lt y<X → ¬y<X (d→∋ X y<X) )
-                         lemma :  ((y : Ordinals.ord O) → (O Ordinals.o< y) x → odef X y → ⊥) ∨ choiced (od→ord X)
+                         lemma :  ((y : Ordinals.ord O) → (O Ordinals.o< y) x → odef X y → ⊥) ∨ choiced (& X)
                          lemma = ∀-imply-or lemma1
-                 have_to_find : choiced (od→ord X)
-                 have_to_find = dont-or  (lemma-ord (od→ord X )) ¬¬X∋x where
-                     ¬¬X∋x : ¬ ((x : Ordinal) → x o< (od→ord X) → odef X x → ⊥)
+                 have_to_find : choiced (& X)
+                 have_to_find = dont-or  (lemma-ord (& X )) ¬¬X∋x where
+                     ¬¬X∋x : ¬ ((x : Ordinal) → x o< (& X) → odef X x → ⊥)
                      ¬¬X∋x nn = not record {
                             eq→ = λ {x} lt → ⊥-elim  (nn x (odef→o< lt) lt) 
                           ; eq← = λ {x} lt → ⊥-elim ( ¬x<0 lt )
@@ -140,7 +136,7 @@
          ... | case1 P =
               record { min = x
                 ;     x∋min = u∋x 
-                ;     min-empty = λ y → P (od→ord y)
+                ;     min-empty = λ y → P (& y)
               } 
          ... | case2 NP =  min2 where
               p : HOD
@@ -149,24 +145,24 @@
                  lemma {y} lt = min1 (<odmax x (proj1 lt)) (<odmax u (proj2 lt))
               np : ¬ (p =h= od∅)
               np p∅ =  NP (λ y p∋y → ∅< {p} {_} (d→∋ p p∋y) p∅ ) 
-              y1choice : choiced (od→ord p)
+              y1choice : choiced (& p)
               y1choice = choice-func p np
               y1 : HOD
-              y1 = ord→od (a-choice y1choice)
+              y1 = * (a-choice y1choice)
               y1prop : (x ∋ y1) ∧ (u ∋ y1)
               y1prop = oo∋ (is-in y1choice)
               min2 : Minimal u
               min2 = prev (proj1 y1prop) u (proj2 y1prop)
          Min2 : (x : HOD) → (u : HOD ) → (u∋x : u ∋ x) → Minimal u 
          Min2 x u u∋x = (ε-induction1 {λ y →  (u : HOD ) → (u∋x : u ∋ y) → Minimal u  } induction x u u∋x ) 
-         cx : {x : HOD} →  ¬ (x =h= od∅ ) → choiced (od→ord x )
+         cx : {x : HOD} →  ¬ (x =h= od∅ ) → choiced (& x )
          cx {x} nx = choice-func x nx
          minimal : (x : HOD  ) → ¬ (x =h= od∅ ) → HOD 
-         minimal x ne = min (Min2 (ord→od (a-choice (cx {x} ne) )) x ( oo∋ (is-in (cx ne))) )
-         x∋minimal : (x : HOD  ) → ( ne : ¬ (x =h= od∅ ) ) → odef x ( od→ord ( minimal x ne ) )
-         x∋minimal x ne = x∋min (Min2 (ord→od (a-choice (cx {x} ne) )) x ( oo∋ (is-in (cx ne))) )
-         minimal-1 : (x : HOD  ) → ( ne : ¬ (x =h= od∅ ) ) → (y : HOD ) → ¬ ( odef (minimal x ne) (od→ord y)) ∧ (odef x (od→ord  y) )
-         minimal-1 x ne y = min-empty (Min2 (ord→od (a-choice (cx ne) )) x ( oo∋ (is-in (cx ne)))) y
+         minimal x ne = min (Min2 (* (a-choice (cx {x} ne) )) x ( oo∋ (is-in (cx ne))) )
+         x∋minimal : (x : HOD  ) → ( ne : ¬ (x =h= od∅ ) ) → odef x ( & ( minimal x ne ) )
+         x∋minimal x ne = x∋min (Min2 (* (a-choice (cx {x} ne) )) x ( oo∋ (is-in (cx ne))) )
+         minimal-1 : (x : HOD  ) → ( ne : ¬ (x =h= od∅ ) ) → (y : HOD ) → ¬ ( odef (minimal x ne) (& y)) ∧ (odef x (&  y) )
+         minimal-1 x ne y = min-empty (Min2 (* (a-choice (cx ne) )) x ( oo∋ (is-in (cx ne)))) y
 
 
 
diff -r cb067605fea0 -r 44a484f17f26 OD.agda
--- a/OD.agda	Fri Jul 31 17:54:52 2020 +0900
+++ b/OD.agda	Sat Aug 01 11:06:29 2020 +0900
@@ -5,7 +5,7 @@
 
 open import zf
 open import Data.Nat renaming ( zero to Zero ; suc to Suc ;  ℕ to Nat ; _⊔_ to _n⊔_ ) 
-open import  Relation.Binary.PropositionalEquality
+open import  Relation.Binary.PropositionalEquality hiding ( [_] )
 open import Data.Nat.Properties 
 open import Data.Empty
 open import Relation.Nullary
@@ -91,17 +91,17 @@
 record ODAxiom : Set (suc n) where      
  field
   -- HOD is isomorphic to Ordinal (by means of Goedel number)
-  od→ord : HOD  → Ordinal 
-  ord→od : Ordinal  → HOD  
-  c<→o<  :  {x y : HOD  }   → def (od y) ( od→ord x ) → od→ord x o< od→ord y
-  ⊆→o≤   :  {y z : HOD  }   → ({x : Ordinal} → def (od y) x → def (od z) x ) → od→ord y o< osuc (od→ord z)
-  oiso   :  {x : HOD }      → ord→od ( od→ord x ) ≡ x
-  diso   :  {x : Ordinal }  → od→ord ( ord→od x ) ≡ x
+  & : HOD  → Ordinal 
+  * : Ordinal  → HOD  
+  c<→o<  :  {x y : HOD  }   → def (od y) ( & x ) → & x o< & y
+  ⊆→o≤   :  {y z : HOD  }   → ({x : Ordinal} → def (od y) x → def (od z) x ) → & y o< osuc (& z)
+  *iso   :  {x : HOD }      → * ( & x ) ≡ x
+  &iso   :  {x : Ordinal }  → & ( * x ) ≡ x
   ==→o≡  :  {x y : HOD  }   → (od x == od y) → x ≡ y
   sup-o  :  (A : HOD) → (     ( x : Ordinal ) → def (od A) x →  Ordinal ) →  Ordinal 
   sup-o< :  (A : HOD) → { ψ : ( x : Ordinal ) → def (od A) x →  Ordinal } → ∀ {x : Ordinal } → (lt : def (od A) x ) → ψ x lt o<  sup-o A ψ 
 -- possible order restriction
-  ho< : {x : HOD} → od→ord x o< next (odmax x)
+  ho< : {x : HOD} → & x o< next (odmax x)
 
 
 postulate  odAxiom : ODAxiom
@@ -118,8 +118,8 @@
 odmaxmin = (y : HOD) (z : Ordinal) → ((x : Ordinal)→ def (od y) x → x o< z) → odmax y o< osuc z
 
 -- OD ⇔ Ordinal leads a contradiction, so we need bounded HOD
-¬OD-order : ( od→ord : OD  → Ordinal ) → ( ord→od : Ordinal  → OD ) → ( { x y : OD  }  → def y ( od→ord x ) → od→ord x o< od→ord y) → ⊥
-¬OD-order od→ord ord→od c<→o< = osuc-< <-osuc (c<→o< {Ords} OneObj )
+¬OD-order : ( & : OD  → Ordinal ) → ( * : Ordinal  → OD ) → ( { x y : OD  }  → def y ( & x ) → & x o< & y) → ⊥
+¬OD-order & * c<→o< = osuc-< <-osuc (c<→o< {Ords} OneObj )
 
 -- Open supreme upper bound leads a contradition, so we use domain restriction on sup
 ¬open-sup : ( sup-o : (Ordinal →  Ordinal ) → Ordinal) → ((ψ : Ordinal →  Ordinal ) → (x : Ordinal) → ψ x  o<  sup-o ψ ) → ⊥
@@ -140,13 +140,13 @@
 odef A x = def ( od A ) x
 
 _∋_ : ( a x : HOD  ) → Set n
-_∋_  a x  = odef a ( od→ord x )
+_∋_  a x  = odef a ( & x )
 
 _c<_ : ( x a : HOD  ) → Set n
 x c< a = a ∋ x 
 
-d→∋ : ( a : HOD  ) { x : Ordinal} → odef a x → a ∋ (ord→od x)
-d→∋ a lt = subst (λ k → odef a k ) (sym diso) lt
+d→∋ : ( a : HOD  ) { x : Ordinal} → odef a x → a ∋ (* x)
+d→∋ a lt = subst (λ k → odef a k ) (sym &iso) lt
 
 cseq :  HOD  →  HOD 
 cseq x = record { od = record { def = λ y → odef x (osuc y) } ; odmax = osuc (odmax x) ; <odmax = lemma } where
@@ -159,60 +159,60 @@
 otrans : {a x y : Ordinal  } → odef (Ord a) x → odef (Ord x) y → odef (Ord a) y
 otrans x<a y<x = ordtrans y<x x<a
 
-odef→o< :  {X : HOD } → {x : Ordinal } → odef X x → x o< od→ord X 
-odef→o<  {X} {x} lt = o<-subst  {_} {_} {x} {od→ord X} ( c<→o< ( odef-subst  {X} {x}  lt (sym oiso) (sym diso) )) diso diso
+odef→o< :  {X : HOD } → {x : Ordinal } → odef X x → x o< & X 
+odef→o<  {X} {x} lt = o<-subst  {_} {_} {x} {& X} ( c<→o< ( odef-subst  {X} {x}  lt (sym *iso) (sym &iso) )) &iso &iso
 
-odefo→o< :  {X y : Ordinal } → odef (ord→od X) y → y o< X
-odefo→o< {X} {y} lt = subst₂ (λ j k → j o< k ) diso diso ( c<→o< (subst (λ k → odef (ord→od X) k ) (sym diso ) lt ))
+odefo→o< :  {X y : Ordinal } → odef (* X) y → y o< X
+odefo→o< {X} {y} lt = subst₂ (λ j k → j o< k ) &iso &iso ( c<→o< (subst (λ k → odef (* X) k ) (sym &iso ) lt ))
 
 -- If we have reverse of c<→o<, everything becomes Ordinal
-o<→c<→HOD=Ord : ( o<→c< : {x y : Ordinal  } → x o< y → odef (ord→od y) x ) → {x : HOD } →  x ≡ Ord (od→ord x)
+o<→c<→HOD=Ord : ( o<→c< : {x y : Ordinal  } → x o< y → odef (* y) x ) → {x : HOD } →  x ≡ Ord (& x)
 o<→c<→HOD=Ord o<→c< {x} = ==→o≡ ( record { eq→ = lemma1 ; eq← = lemma2 } ) where
-   lemma1 : {y : Ordinal} → odef x y → odef (Ord (od→ord x)) y
-   lemma1 {y} lt = subst ( λ k → k o< od→ord x ) diso (c<→o< {ord→od y} {x} (d→∋ x lt))
-   lemma2 : {y : Ordinal} → odef (Ord (od→ord x)) y → odef x y
-   lemma2 {y} lt = subst (λ k → odef k y ) oiso (o<→c< {y} {od→ord x} lt )
+   lemma1 : {y : Ordinal} → odef x y → odef (Ord (& x)) y
+   lemma1 {y} lt = subst ( λ k → k o< & x ) &iso (c<→o< {* y} {x} (d→∋ x lt))
+   lemma2 : {y : Ordinal} → odef (Ord (& x)) y → odef x y
+   lemma2 {y} lt = subst (λ k → odef k y ) *iso (o<→c< {y} {& x} lt )
 
 -- avoiding lv != Zero error
-orefl : { x : HOD  } → { y : Ordinal  } → od→ord x ≡ y → od→ord x ≡ y
+orefl : { x : HOD  } → { y : Ordinal  } → & x ≡ y → & x ≡ y
 orefl refl = refl
 
-==-iso : { x y : HOD  } → od (ord→od (od→ord x)) == od (ord→od (od→ord y))  →  od x == od y
+==-iso : { x y : HOD  } → od (* (& x)) == od (* (& y))  →  od x == od y
 ==-iso  {x} {y} eq = record {
-      eq→ = λ d →  lemma ( eq→  eq (odef-subst d (sym oiso) refl )) ;
-      eq← = λ d →  lemma ( eq←  eq (odef-subst d (sym oiso) refl ))  }
+      eq→ = λ d →  lemma ( eq→  eq (odef-subst d (sym *iso) refl )) ;
+      eq← = λ d →  lemma ( eq←  eq (odef-subst d (sym *iso) refl ))  }
         where
-           lemma : {x : HOD  } {z : Ordinal } → odef (ord→od (od→ord x)) z → odef x z
-           lemma {x} {z} d = odef-subst d oiso refl
+           lemma : {x : HOD  } {z : Ordinal } → odef (* (& x)) z → odef x z
+           lemma {x} {z} d = odef-subst d *iso refl
 
-=-iso :  {x y : HOD  } → (od x == od y) ≡ (od (ord→od (od→ord x)) == od y)
-=-iso  {_} {y} = cong ( λ k → od k == od y ) (sym oiso)
+=-iso :  {x y : HOD  } → (od x == od y) ≡ (od (* (& x)) == od y)
+=-iso  {_} {y} = cong ( λ k → od k == od y ) (sym *iso)
 
-ord→== : { x y : HOD  } → od→ord x ≡  od→ord y →  od x == od y
-ord→==  {x} {y} eq = ==-iso (lemma (od→ord x) (od→ord y) (orefl eq)) where
-   lemma : ( ox oy : Ordinal  ) → ox ≡ oy →  od (ord→od ox) == od (ord→od oy)
+ord→== : { x y : HOD  } → & x ≡  & y →  od x == od y
+ord→==  {x} {y} eq = ==-iso (lemma (& x) (& y) (orefl eq)) where
+   lemma : ( ox oy : Ordinal  ) → ox ≡ oy →  od (* ox) == od (* oy)
    lemma ox ox  refl = ==-refl
 
-o≡→== : { x y : Ordinal  } → x ≡  y →  od (ord→od x) == od (ord→od y)
+o≡→== : { x y : Ordinal  } → x ≡  y →  od (* x) == od (* y)
 o≡→==  {x} {.x} refl = ==-refl
 
-o∅≡od∅ : ord→od (o∅ ) ≡ od∅ 
+o∅≡od∅ : * (o∅ ) ≡ od∅ 
 o∅≡od∅  = ==→o≡ lemma where
-     lemma0 :  {x : Ordinal} → odef (ord→od o∅) x → odef od∅ x
-     lemma0 {x} lt = o<-subst (c<→o<  {ord→od x} {ord→od o∅} (odef-subst  {ord→od o∅} {x} lt refl (sym diso)) ) diso diso
-     lemma1 :  {x : Ordinal} → odef od∅ x → odef (ord→od o∅) x
+     lemma0 :  {x : Ordinal} → odef (* o∅) x → odef od∅ x
+     lemma0 {x} lt = o<-subst (c<→o<  {* x} {* o∅} (odef-subst  {* o∅} {x} lt refl (sym &iso)) ) &iso &iso
+     lemma1 :  {x : Ordinal} → odef od∅ x → odef (* o∅) x
      lemma1 {x} lt = ⊥-elim (¬x<0 lt)
-     lemma : od (ord→od o∅) == od od∅
+     lemma : od (* o∅) == od od∅
      lemma = record { eq→ = lemma0 ; eq← = lemma1 }
 
-ord-od∅ : od→ord (od∅ ) ≡ o∅ 
-ord-od∅  = sym ( subst (λ k → k ≡  od→ord (od∅ ) ) diso (cong ( λ k → od→ord k ) o∅≡od∅ ) )
+ord-od∅ : & (od∅ ) ≡ o∅ 
+ord-od∅  = sym ( subst (λ k → k ≡  & (od∅ ) ) &iso (cong ( λ k → & k ) o∅≡od∅ ) )
 
 ∅0 : record { def = λ x →  Lift n ⊥ } == od od∅  
 eq→ ∅0 {w} (lift ())
 eq← ∅0 {w} lt = lift (¬x<0 lt)
 
-∅< : { x y : HOD  } → odef x (od→ord y ) → ¬ (  od x  == od od∅  )
+∅< : { x y : HOD  } → odef x (& y ) → ¬ (  od x  == od od∅  )
 ∅<  {x} {y} d eq with eq→ (==-trans eq (==-sym ∅0) ) d
 ∅<  {x} {y} d eq | lift ()
        
@@ -230,44 +230,44 @@
 
 -- the pair
 _,_ : HOD  → HOD  → HOD  
-x , y = record { od = record { def = λ t → (t ≡ od→ord x ) ∨ ( t ≡ od→ord y ) } ; odmax = omax (od→ord x)  (od→ord y) ; <odmax = lemma }  where
-    lemma : {t : Ordinal} → (t ≡ od→ord x) ∨ (t ≡ od→ord y) → t o< omax (od→ord x) (od→ord y)
+x , y = record { od = record { def = λ t → (t ≡ & x ) ∨ ( t ≡ & y ) } ; odmax = omax (& x)  (& y) ; <odmax = lemma }  where
+    lemma : {t : Ordinal} → (t ≡ & x) ∨ (t ≡ & y) → t o< omax (& x) (& y)
     lemma {t} (case1 refl) = omax-x  _ _
     lemma {t} (case2 refl) = omax-y  _ _
 
-pair-xx<xy : {x y : HOD} → od→ord (x , x) o< osuc (od→ord (x , y) )
+pair-xx<xy : {x y : HOD} → & (x , x) o< osuc (& (x , y) )
 pair-xx<xy {x} {y} = ⊆→o≤  lemma where
    lemma : {z : Ordinal} → def (od (x , x)) z → def (od (x , y)) z
    lemma {z} (case1 refl) = case1 refl
    lemma {z} (case2 refl) = case1 refl
 
-pair-<xy : {x y : HOD} → {n : Ordinal}  → od→ord x o< next n →  od→ord y o< next n  → od→ord (x , y) o< next n
-pair-<xy {x} {y} {o} x<nn y<nn with trio< (od→ord x) (od→ord y) | inspect (omax (od→ord x)) (od→ord y)
+pair-<xy : {x y : HOD} → {n : Ordinal}  → & x o< next n →  & y o< next n  → & (x , y) o< next n
+pair-<xy {x} {y} {o} x<nn y<nn with trio< (& x) (& y) | inspect (omax (& x)) (& y)
 ... | tri< a ¬b ¬c | record { eq = eq1 } = next< (subst (λ k → k o< next o ) (sym eq1) (osuc<nx y<nn)) ho< 
 ... | tri> ¬a ¬b c | record { eq = eq1 } = next< (subst (λ k → k o< next o ) (sym eq1) (osuc<nx x<nn)) ho< 
 ... | tri≈ ¬a b ¬c | record { eq = eq1 } = next< (subst (λ k → k o< next o ) (omax≡ _ _ b) (subst (λ k → osuc k o< next o) b (osuc<nx x<nn))) ho< 
 
 --  another form of infinite
 -- pair-ord< :  {x : Ordinal } → Set n
-pair-ord< : {x : HOD } → ( {y : HOD } → od→ord y o< next (odmax y) ) → od→ord ( x , x ) o< next (od→ord x)
-pair-ord< {x} ho< = subst (λ k → od→ord (x , x) o< k ) lemmab0 lemmab1  where
-       lemmab0 : next (odmax (x , x)) ≡ next (od→ord x)
+pair-ord< : {x : HOD } → ( {y : HOD } → & y o< next (odmax y) ) → & ( x , x ) o< next (& x)
+pair-ord< {x} ho< = subst (λ k → & (x , x) o< k ) lemmab0 lemmab1  where
+       lemmab0 : next (odmax (x , x)) ≡ next (& x)
        lemmab0 = trans (cong (λ k → next k) (omxx _)) (sym nexto≡)
-       lemmab1 : od→ord (x , x) o< next ( odmax (x , x))
+       lemmab1 : & (x , x) o< next ( odmax (x , x))
        lemmab1 = ho<
 
-pair<y : {x y : HOD } → y ∋ x  → od→ord (x , x) o< osuc (od→ord y)
+pair<y : {x y : HOD } → y ∋ x  → & (x , x) o< osuc (& y)
 pair<y {x} {y} y∋x = ⊆→o≤ lemma where
    lemma : {z : Ordinal} → def (od (x , x)) z → def (od y) z
    lemma (case1 refl) = y∋x
    lemma (case2 refl) = y∋x
 
 -- another possible restriction. We reqest no minimality on odmax, so it may arbitrary larger.
-odmax<od→ord  : { x y : HOD } → x ∋ y →  Set n
-odmax<od→ord {x} {y} x∋y = odmax x o< od→ord x
+odmax<&  : { x y : HOD } → x ∋ y →  Set n
+odmax<& {x} {y} x∋y = odmax x o< & x
 
 in-codomain : (X : HOD  ) → ( ψ : HOD  → HOD  ) → OD 
-in-codomain  X ψ = record { def = λ x → ¬ ( (y : Ordinal ) → ¬ ( odef X y ∧  ( x ≡ od→ord (ψ (ord→od y )))))  }
+in-codomain  X ψ = record { def = λ x → ¬ ( (y : Ordinal ) → ¬ ( odef X y ∧  ( x ≡ & (ψ (* y )))))  }
 
 _∩_ : ( A B : HOD ) → HOD 
 A ∩ B = record { od = record { def = λ x → odef A x ∧ odef B x }
@@ -286,35 +286,35 @@
 refl-⊆ : {A : HOD} → A ⊆ A
 refl-⊆ {A} = record { incl = λ x → x }
 
-od⊆→o≤  : {x y : HOD } → x ⊆ y → od→ord x o< osuc (od→ord y)
-od⊆→o≤ {x} {y} lt  =  ⊆→o≤ {x} {y} (λ {z} x>z  → subst (λ k → def (od y) k ) diso (incl lt (d→∋ x x>z)))
+od⊆→o≤  : {x y : HOD } → x ⊆ y → & x o< osuc (& y)
+od⊆→o≤ {x} {y} lt  =  ⊆→o≤ {x} {y} (λ {z} x>z  → subst (λ k → def (od y) k ) &iso (incl lt (d→∋ x x>z)))
 
--- if we have od→ord (x , x) ≡ osuc (od→ord x),  ⊆→o≤ → c<→o<
-⊆→o≤→c<→o< : ({x : HOD} → od→ord (x , x) ≡ osuc (od→ord x) )
-   →  ({y z : HOD  }   → ({x : Ordinal} → def (od y) x → def (od z) x ) → od→ord y o< osuc (od→ord z) )
-   →   {x y : HOD  }   → def (od y) ( od→ord x ) → od→ord x o< od→ord y 
-⊆→o≤→c<→o< peq ⊆→o≤ {x} {y} y∋x with trio< (od→ord x) (od→ord y)
+-- if we have & (x , x) ≡ osuc (& x),  ⊆→o≤ → c<→o<
+⊆→o≤→c<→o< : ({x : HOD} → & (x , x) ≡ osuc (& x) )
+   →  ({y z : HOD  }   → ({x : Ordinal} → def (od y) x → def (od z) x ) → & y o< osuc (& z) )
+   →   {x y : HOD  }   → def (od y) ( & x ) → & x o< & y 
+⊆→o≤→c<→o< peq ⊆→o≤ {x} {y} y∋x with trio< (& x) (& y)
 ⊆→o≤→c<→o< peq ⊆→o≤ {x} {y} y∋x | tri< a ¬b ¬c = a
 ⊆→o≤→c<→o< peq ⊆→o≤ {x} {y} y∋x | tri≈ ¬a b ¬c = ⊥-elim ( o<¬≡ (peq {x}) (pair<y (subst (λ k → k ∋ x) (sym ( ==→o≡ {x} {y} (ord→== b))) y∋x )))
 ⊆→o≤→c<→o< peq ⊆→o≤ {x} {y} y∋x | tri> ¬a ¬b c =
   ⊥-elim ( o<> (⊆→o≤ {x , x} {y} y⊆x,x ) lemma1 ) where
-    lemma : {z : Ordinal} → (z ≡ od→ord x) ∨ (z ≡ od→ord x) → od→ord x ≡ z
+    lemma : {z : Ordinal} → (z ≡ & x) ∨ (z ≡ & x) → & x ≡ z
     lemma (case1 refl) = refl
     lemma (case2 refl) = refl
     y⊆x,x : {z : Ordinals.ord O} → def (od (x , x)) z → def (od y) z
     y⊆x,x {z} lt = subst (λ k → def (od y) k ) (lemma lt) y∋x 
-    lemma1 : osuc (od→ord y) o< od→ord (x , x)
-    lemma1 = subst (λ k → osuc (od→ord y) o< k ) (sym (peq {x})) (osucc c ) 
+    lemma1 : osuc (& y) o< & (x , x)
+    lemma1 = subst (λ k → osuc (& y) o< k ) (sym (peq {x})) (osucc c ) 
 
 subset-lemma : {A x : HOD  } → ( {y : HOD } →  x ∋ y → (A ∩ x ) ∋  y ) ⇔  ( x ⊆ A  )
 subset-lemma  {A} {x} = record {
       proj1 = λ lt  → record { incl = λ x∋z → proj1 (lt x∋z)  }
-    ; proj2 = λ x⊆A lt → record { proj1 = incl x⊆A lt ; proj2 = lt } 
+    ; proj2 = λ x⊆A lt → ⟪ incl x⊆A lt , lt ⟫
    } 
 
-power< : {A x : HOD  } → x ⊆ A → Ord (osuc (od→ord A)) ∋ x
-power< {A} {x} x⊆A = ⊆→o≤  (λ {y} x∋y → subst (λ k →  def (od A) k) diso (lemma y x∋y ) ) where
-    lemma : (y : Ordinal) → def (od x) y → def (od A) (od→ord (ord→od y))
+power< : {A x : HOD  } → x ⊆ A → Ord (osuc (& A)) ∋ x
+power< {A} {x} x⊆A = ⊆→o≤  (λ {y} x∋y → subst (λ k →  def (od A) k) &iso (lemma y x∋y ) ) where
+    lemma : (y : Ordinal) → def (od x) y → def (od A) (& (* y))
     lemma y x∋y = incl x⊆A (d→∋ x x∋y)
 
 open import Data.Unit
@@ -322,30 +322,30 @@
 ε-induction : { ψ : HOD  → Set n}
    → ( {x : HOD } → ({ y : HOD } →  x ∋ y → ψ y ) → ψ x )
    → (x : HOD ) → ψ x
-ε-induction {ψ} ind x = subst (λ k → ψ k ) oiso (ε-induction-ord (osuc (od→ord x)) <-osuc )  where
-     induction : (ox : Ordinal) → ((oy : Ordinal) → oy o< ox → ψ (ord→od oy)) → ψ (ord→od ox)
-     induction ox prev = ind  ( λ {y} lt → subst (λ k → ψ k ) oiso (prev (od→ord y) (o<-subst (c<→o< lt) refl diso ))) 
-     ε-induction-ord : (ox : Ordinal) { oy : Ordinal } → oy o< ox → ψ (ord→od oy)
-     ε-induction-ord ox {oy} lt = TransFinite {λ oy → ψ (ord→od oy)} induction oy
+ε-induction {ψ} ind x = subst (λ k → ψ k ) *iso (ε-induction-ord (osuc (& x)) <-osuc )  where
+     induction : (ox : Ordinal) → ((oy : Ordinal) → oy o< ox → ψ (* oy)) → ψ (* ox)
+     induction ox prev = ind  ( λ {y} lt → subst (λ k → ψ k ) *iso (prev (& y) (o<-subst (c<→o< lt) refl &iso ))) 
+     ε-induction-ord : (ox : Ordinal) { oy : Ordinal } → oy o< ox → ψ (* oy)
+     ε-induction-ord ox {oy} lt = TransFinite {λ oy → ψ (* oy)} induction oy
 
 -- level trick (what'a shame) for LEM / minimal
 ε-induction1 : { ψ : HOD  → Set (suc n)}
    → ( {x : HOD } → ({ y : HOD } →  x ∋ y → ψ y ) → ψ x )
    → (x : HOD ) → ψ x
-ε-induction1 {ψ} ind x = subst (λ k → ψ k ) oiso (ε-induction-ord (osuc (od→ord x)) <-osuc )  where
-     induction : (ox : Ordinal) → ((oy : Ordinal) → oy o< ox → ψ (ord→od oy)) → ψ (ord→od ox)
-     induction ox prev = ind  ( λ {y} lt → subst (λ k → ψ k ) oiso (prev (od→ord y) (o<-subst (c<→o< lt) refl diso ))) 
-     ε-induction-ord : (ox : Ordinal) { oy : Ordinal } → oy o< ox → ψ (ord→od oy)
-     ε-induction-ord ox {oy} lt = TransFinite1 {λ oy → ψ (ord→od oy)} induction oy
+ε-induction1 {ψ} ind x = subst (λ k → ψ k ) *iso (ε-induction-ord (osuc (& x)) <-osuc )  where
+     induction : (ox : Ordinal) → ((oy : Ordinal) → oy o< ox → ψ (* oy)) → ψ (* ox)
+     induction ox prev = ind  ( λ {y} lt → subst (λ k → ψ k ) *iso (prev (& y) (o<-subst (c<→o< lt) refl &iso ))) 
+     ε-induction-ord : (ox : Ordinal) { oy : Ordinal } → oy o< ox → ψ (* oy)
+     ε-induction-ord ox {oy} lt = TransFinite1 {λ oy → ψ (* oy)} induction oy
 
 Select : (X : HOD  ) → ((x : HOD  ) → Set n ) → HOD 
-Select X ψ = record { od = record { def = λ x →  ( odef X x ∧ ψ ( ord→od x )) } ; odmax = odmax X ; <odmax = λ y → <odmax X (proj1 y) }
+Select X ψ = record { od = record { def = λ x →  ( odef X x ∧ ψ ( * x )) } ; odmax = odmax X ; <odmax = λ y → <odmax X (proj1 y) }
 
 Replace : HOD  → (HOD  → HOD) → HOD 
-Replace X ψ = record { od = record { def = λ x → (x o< sup-o X (λ y X∋y → od→ord (ψ (ord→od y)))) ∧ def (in-codomain X ψ) x }
+Replace X ψ = record { od = record { def = λ x → (x o< sup-o X (λ y X∋y → & (ψ (* y)))) ∧ def (in-codomain X ψ) x }
     ; odmax = rmax ; <odmax = rmax<} where 
         rmax : Ordinal
-        rmax = sup-o X (λ y X∋y → od→ord (ψ (ord→od y)))
+        rmax = sup-o X (λ y X∋y → & (ψ (* y)))
         rmax< :  {y : Ordinal} → (y o< rmax) ∧ def (in-codomain X ψ) y → y o< rmax
         rmax< lt = proj1 lt
 
@@ -353,28 +353,28 @@
 -- If we have LEM, Replace' is equivalent to Replace 
 --
 in-codomain' : (X : HOD  ) → ((x : HOD) → X ∋ x → HOD) → OD 
-in-codomain'  X ψ = record { def = λ x → ¬ ( (y : Ordinal ) → ¬ ( odef X y ∧  ((lt : odef X y) →  x ≡ od→ord (ψ (ord→od y ) (d→∋ X lt) ))))  }
+in-codomain'  X ψ = record { def = λ x → ¬ ( (y : Ordinal ) → ¬ ( odef X y ∧  ((lt : odef X y) →  x ≡ & (ψ (* y ) (d→∋ X lt) ))))  }
 Replace' : (X : HOD)  → ((x : HOD) → X ∋ x → HOD) → HOD 
-Replace' X ψ = record { od = record { def = λ x → (x o< sup-o X (λ y X∋y → od→ord (ψ (ord→od y) (d→∋ X X∋y) ))) ∧ def (in-codomain' X ψ) x }
+Replace' X ψ = record { od = record { def = λ x → (x o< sup-o X (λ y X∋y → & (ψ (* y) (d→∋ X X∋y) ))) ∧ def (in-codomain' X ψ) x }
       ; odmax = rmax ; <odmax = rmax< } where
         rmax : Ordinal
-        rmax = sup-o X (λ y X∋y → od→ord (ψ (ord→od y) (d→∋ X X∋y)))
+        rmax = sup-o X (λ y X∋y → & (ψ (* y) (d→∋ X X∋y)))
         rmax< :  {y : Ordinal} → (y o< rmax) ∧ def (in-codomain' X ψ) y → y o< rmax
         rmax< lt = proj1 lt
 
 Union : HOD  → HOD   
-Union U = record { od = record { def = λ x → ¬ (∀ (u : Ordinal ) → ¬ ((odef U u) ∧ (odef (ord→od u) x)))  }
-    ; odmax = osuc (od→ord U) ; <odmax = umax< } where
-        umax< :  {y : Ordinal} → ¬ ((u : Ordinal) → ¬ def (od U) u ∧ def (od (ord→od u)) y) → y o< osuc (od→ord U)
+Union U = record { od = record { def = λ x → ¬ (∀ (u : Ordinal ) → ¬ ((odef U u) ∧ (odef (* u) x)))  }
+    ; odmax = osuc (& U) ; <odmax = umax< } where
+        umax< :  {y : Ordinal} → ¬ ((u : Ordinal) → ¬ def (od U) u ∧ def (od (* u)) y) → y o< osuc (& U)
         umax< {y} not = lemma (FExists _ lemma1 not ) where
-            lemma0 : {x : Ordinal} → def (od (ord→od x)) y → y o< x
-            lemma0 {x} x<y = subst₂ (λ j k → j o< k ) diso  diso (c<→o< (d→∋ (ord→od x) x<y ))
-            lemma2 : {x : Ordinal} → def (od U) x → x o< od→ord U
-            lemma2 {x} x<U = subst (λ k → k o< od→ord U ) diso (c<→o< (d→∋ U x<U)) 
-            lemma1 : {x : Ordinal} → def (od U) x ∧ def (od (ord→od x)) y → ¬ (od→ord U o< y)
+            lemma0 : {x : Ordinal} → def (od (* x)) y → y o< x
+            lemma0 {x} x<y = subst₂ (λ j k → j o< k ) &iso  &iso (c<→o< (d→∋ (* x) x<y ))
+            lemma2 : {x : Ordinal} → def (od U) x → x o< & U
+            lemma2 {x} x<U = subst (λ k → k o< & U ) &iso (c<→o< (d→∋ U x<U)) 
+            lemma1 : {x : Ordinal} → def (od U) x ∧ def (od (* x)) y → ¬ (& U o< y)
             lemma1 {x} lt u<y = o<> u<y (ordtrans (lemma0 (proj2 lt)) (lemma2 (proj1 lt)) )
-            lemma : ¬ ((od→ord U) o< y ) → y o< osuc (od→ord U)
-            lemma not with trio< y (od→ord U)
+            lemma : ¬ ((& U) o< y ) → y o< osuc (& U)
+            lemma not with trio< y (& U)
             lemma not | tri< a ¬b ¬c = ordtrans a <-osuc
             lemma not | tri≈ ¬a refl ¬c = <-osuc
             lemma not | tri> ¬a ¬b c = ⊥-elim (not c)
@@ -382,31 +382,31 @@
 A ∈ B = B ∋ A
 
 OPwr :  (A :  HOD ) → HOD 
-OPwr  A = Ord ( sup-o (Ord (osuc (od→ord A))) ( λ x A∋x → od→ord ( A ∩ (ord→od x)) ) )   
+OPwr  A = Ord ( sup-o (Ord (osuc (& A))) ( λ x A∋x → & ( A ∩ (* x)) ) )   
 
 Power : HOD  → HOD 
-Power A = Replace (OPwr (Ord (od→ord A))) ( λ x → A ∩ x )
+Power A = Replace (OPwr (Ord (& A))) ( λ x → A ∩ x )
 -- ｛_｝ : ZFSet → ZFSet
 -- ｛ x ｝ = ( x ,  x )     -- better to use (x , x) directly
 
 union→ :  (X z u : HOD) → (X ∋ u) ∧ (u ∋ z) → Union X ∋ z
-union→ X z u xx not = ⊥-elim ( not (od→ord u) ( record { proj1 = proj1 xx
-    ; proj2 = subst ( λ k → odef k (od→ord z)) (sym oiso) (proj2 xx) } ))
+union→ X z u xx not = ⊥-elim ( not (& u) ( ⟪ proj1 xx
+    , subst ( λ k → odef k (& z)) (sym *iso) (proj2 xx) ⟫ ))
 union← :  (X z : HOD) (X∋z : Union X ∋ z) →  ¬  ( (u : HOD ) → ¬ ((X ∋  u) ∧ (u ∋ z )))
 union← X z UX∋z =  FExists _ lemma UX∋z where
-    lemma : {y : Ordinal} → odef X y ∧ odef (ord→od y) (od→ord z) → ¬ ((u : HOD) → ¬ (X ∋ u) ∧ (u ∋ z))
-    lemma {y} xx not = not (ord→od y) record { proj1 = d→∋ X (proj1 xx) ; proj2 = proj2 xx } 
+    lemma : {y : Ordinal} → odef X y ∧ odef (* y) (& z) → ¬ ((u : HOD) → ¬ (X ∋ u) ∧ (u ∋ z))
+    lemma {y} xx not = not (* y) ⟪ d→∋ X (proj1 xx) , proj2 xx ⟫
 
 data infinite-d  : ( x : Ordinal  ) → Set n where
     iφ :  infinite-d o∅
     isuc : {x : Ordinal  } →   infinite-d  x  →
-            infinite-d  (od→ord ( Union (ord→od x , (ord→od x , ord→od x ) ) ))
+            infinite-d  (& ( Union (* x , (* x , * x ) ) ))
 
 -- ω can be diverged in our case, since we have no restriction on the corresponding ordinal of a pair.
 -- We simply assumes infinite-d y has a maximum.
 -- 
--- This means that many of OD may not be HODs because of the od→ord mapping divergence.
--- We should have some axioms to prevent this such as od→ord x o< next (odmax x).
+-- This means that many of OD may not be HODs because of the & mapping divergence.
+-- We should have some axioms to prevent this such as & x o< next (odmax x).
 -- 
 -- postulate
 --     ωmax : Ordinal
@@ -421,25 +421,25 @@
 infinite : HOD 
 infinite = record { od = record { def = λ x → infinite-d x } ; odmax = next o∅ ; <odmax = lemma }  where
     u : (y : Ordinal ) → HOD
-    u y = Union (ord→od y , (ord→od y , ord→od y))
+    u y = Union (* y , (* y , * y))
     --   next< : {x y z : Ordinal} → x o< next z  → y o< next x → y o< next z
-    lemma8 : {y : Ordinal} → od→ord (ord→od y , ord→od y) o< next (odmax (ord→od y , ord→od y))
+    lemma8 : {y : Ordinal} → & (* y , * y) o< next (odmax (* y , * y))
     lemma8 = ho<
     ---           (x,y) < next (omax x y) < next (osuc y) = next y 
-    lemmaa : {x y : HOD} → od→ord x o< od→ord y → od→ord (x , y) o< next (od→ord y)
-    lemmaa {x} {y} x<y = subst (λ k → od→ord (x , y) o< k ) (sym nexto≡) (subst (λ k → od→ord (x , y) o< next k ) (sym (omax< _ _ x<y)) ho< )
-    lemma81 : {y : Ordinal} → od→ord (ord→od y , ord→od y) o< next (od→ord (ord→od y))
-    lemma81 {y} = nexto=n (subst (λ k →  od→ord (ord→od y , ord→od y) o< k ) (cong (λ k → next k) (omxx _)) lemma8)
-    lemma9 : {y : Ordinal} → od→ord (ord→od y , (ord→od y , ord→od y)) o< next (od→ord (ord→od y , ord→od y))
+    lemmaa : {x y : HOD} → & x o< & y → & (x , y) o< next (& y)
+    lemmaa {x} {y} x<y = subst (λ k → & (x , y) o< k ) (sym nexto≡) (subst (λ k → & (x , y) o< next k ) (sym (omax< _ _ x<y)) ho< )
+    lemma81 : {y : Ordinal} → & (* y , * y) o< next (& (* y))
+    lemma81 {y} = nexto=n (subst (λ k →  & (* y , * y) o< k ) (cong (λ k → next k) (omxx _)) lemma8)
+    lemma9 : {y : Ordinal} → & (* y , (* y , * y)) o< next (& (* y , * y))
     lemma9 = lemmaa (c<→o< (case1 refl))
-    lemma71 : {y : Ordinal} → od→ord (ord→od y , (ord→od y , ord→od y)) o< next (od→ord (ord→od y))
+    lemma71 : {y : Ordinal} → & (* y , (* y , * y)) o< next (& (* y))
     lemma71 = next< lemma81 lemma9
-    lemma1 : {y : Ordinal} → od→ord (u y) o< next (osuc (od→ord (ord→od y , (ord→od y , ord→od y))))
+    lemma1 : {y : Ordinal} → & (u y) o< next (osuc (& (* y , (* y , * y))))
     lemma1 = ho<
     --- main recursion
     lemma : {y : Ordinal} → infinite-d y → y o< next o∅
     lemma {o∅} iφ = x<nx
-    lemma (isuc {y} x) = next< (lemma x) (next< (subst (λ k → od→ord (ord→od y , (ord→od y , ord→od y)) o< next k) diso lemma71 ) (nexto=n lemma1))
+    lemma (isuc {y} x) = next< (lemma x) (next< (subst (λ k → & (* y , (* y , * y)) o< next k) &iso lemma71 ) (nexto=n lemma1))
 
 ω<next-o∅ : {y : Ordinal} → infinite-d y → y o< next o∅
 ω<next-o∅ {y} lt = <odmax infinite lt
@@ -455,11 +455,11 @@
 ω→nat : (n : HOD) → infinite ∋ n → Nat
 ω→nat n = ω→nato 
 
-ω∋nat→ω : {n : Nat} → def (od infinite) (od→ord (nat→ω n))
+ω∋nat→ω : {n : Nat} → def (od infinite) (& (nat→ω n))
 ω∋nat→ω {Zero} = subst (λ k → def (od infinite) k) (sym ord-od∅) iφ
 ω∋nat→ω {Suc n} = subst (λ k → def (od infinite) k) lemma (isuc ( ω∋nat→ω {n})) where
-    lemma :  od→ord (Union (ord→od (od→ord (nat→ω n)) , (ord→od (od→ord (nat→ω n)) , ord→od (od→ord (nat→ω n))))) ≡ od→ord (nat→ω (Suc n))
-    lemma = subst (λ k → od→ord (Union (k , ( k , k ))) ≡ od→ord (nat→ω (Suc n))) (sym oiso) refl
+    lemma :  & (Union (* (& (nat→ω n)) , (* (& (nat→ω n)) , * (& (nat→ω n))))) ≡ & (nat→ω (Suc n))
+    lemma = subst (λ k → & (Union (k , ( k , k ))) ≡ & (nat→ω (Suc n))) (sym *iso) refl
 
 _=h=_ : (x y : HOD) → Set n
 x =h= y  = od x == od y
@@ -468,12 +468,12 @@
 -- infixr  230 _∩_ _∪_
 
 pair→ : ( x y t : HOD  ) →  (x , y)  ∋ t  → ( t =h= x ) ∨ ( t =h= y ) 
-pair→ x y t (case1 t≡x ) = case1 (subst₂ (λ j k → j =h= k ) oiso oiso (o≡→== t≡x ))
-pair→ x y t (case2 t≡y ) = case2 (subst₂ (λ j k → j =h= k ) oiso oiso (o≡→== t≡y ))
+pair→ x y t (case1 t≡x ) = case1 (subst₂ (λ j k → j =h= k ) *iso *iso (o≡→== t≡x ))
+pair→ x y t (case2 t≡y ) = case2 (subst₂ (λ j k → j =h= k ) *iso *iso (o≡→== t≡y ))
 
 pair← : ( x y t : HOD  ) → ( t =h= x ) ∨ ( t =h= y ) →  (x , y)  ∋ t  
-pair← x y t (case1 t=h=x) = case1 (cong (λ k → od→ord k ) (==→o≡ t=h=x))
-pair← x y t (case2 t=h=y) = case2 (cong (λ k → od→ord k ) (==→o≡ t=h=y))
+pair← x y t (case1 t=h=x) = case1 (cong (λ k → & k ) (==→o≡ t=h=x))
+pair← x y t (case2 t=h=y) = case2 (cong (λ k → & k ) (==→o≡ t=h=y))
 
 pair1 : { x y  : HOD  } →  (x , y ) ∋ x
 pair1 = case1 refl
@@ -495,109 +495,109 @@
 ⊆→o< {x} {y}  lt with trio< x y 
 ⊆→o< {x} {y}  lt | tri< a ¬b ¬c = ordtrans a <-osuc
 ⊆→o< {x} {y}  lt | tri≈ ¬a b ¬c = subst ( λ k → k o< osuc y) (sym b) <-osuc
-⊆→o< {x} {y}  lt | tri> ¬a ¬b c with (incl lt)  (o<-subst c (sym diso) refl )
-... | ttt = ⊥-elim ( o<¬≡ refl (o<-subst ttt diso refl ))
+⊆→o< {x} {y}  lt | tri> ¬a ¬b c with (incl lt)  (o<-subst c (sym &iso) refl )
+... | ttt = ⊥-elim ( o<¬≡ refl (o<-subst ttt &iso refl ))
 
 open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) 
 -- postulate f-extensionality : { n m : Level}  → HE.Extensionality n m
 
-ω-prev-eq1 : {x y : Ordinal} →  od→ord (Union (ord→od y , (ord→od y , ord→od y))) ≡ od→ord (Union (ord→od x , (ord→od x , ord→od x))) → ¬ (x o< y)
-ω-prev-eq1 {x} {y} eq x<y = eq→ (ord→== eq) {od→ord (ord→od y)} (λ not2 → not2 (od→ord (ord→od y , ord→od y))
-      record { proj1 = case2 refl ; proj2 = subst (λ k → odef k (od→ord (ord→od y))) (sym oiso) (case1 refl)} ) (λ u → lemma u ) where
-   lemma : (u : Ordinal) → ¬ def (od (ord→od x , (ord→od x , ord→od x))) u ∧ def (od (ord→od u)) (od→ord (ord→od y))
+ω-prev-eq1 : {x y : Ordinal} →  & (Union (* y , (* y , * y))) ≡ & (Union (* x , (* x , * x))) → ¬ (x o< y)
+ω-prev-eq1 {x} {y} eq x<y = eq→ (ord→== eq) {& (* y)} (λ not2 → not2 (& (* y , * y))
+      ⟪ case2 refl , subst (λ k → odef k (& (* y))) (sym *iso) (case1 refl)⟫ ) (λ u → lemma u ) where
+   lemma : (u : Ordinal) → ¬ def (od (* x , (* x , * x))) u ∧ def (od (* u)) (& (* y))
    lemma u t with proj1 t
-   lemma u t | case1 u=x = o<> (c<→o< {ord→od y} {ord→od u} (proj2 t)) (subst₂ (λ j k → j o< k )
-        (trans (sym diso) (trans (sym u=x) (sym diso)) ) (sym diso) x<y ) -- x ≡ od→ord (ord→od u)
-   lemma u t | case2 u=xx = o<¬≡ (lemma1 (subst (λ k → odef k (od→ord (ord→od y)) ) (trans (cong (λ k → ord→od k ) u=xx) oiso )  (proj2 t))) x<y where
-       lemma1 : {x y : Ordinal } → (ord→od x , ord→od x ) ∋ ord→od y → x ≡ y    --  y = x ∈ ( x , x ) = u 
-       lemma1 (case1 eq) = subst₂ (λ j k → j ≡ k ) diso diso (sym eq)
-       lemma1 (case2 eq) = subst₂ (λ j k → j ≡ k ) diso diso (sym eq)
+   lemma u t | case1 u=x = o<> (c<→o< {* y} {* u} (proj2 t)) (subst₂ (λ j k → j o< k )
+        (trans (sym &iso) (trans (sym u=x) (sym &iso)) ) (sym &iso) x<y ) -- x ≡ & (* u)
+   lemma u t | case2 u=xx = o<¬≡ (lemma1 (subst (λ k → odef k (& (* y)) ) (trans (cong (λ k → * k ) u=xx) *iso )  (proj2 t))) x<y where
+       lemma1 : {x y : Ordinal } → (* x , * x ) ∋ * y → x ≡ y    --  y = x ∈ ( x , x ) = u 
+       lemma1 (case1 eq) = subst₂ (λ j k → j ≡ k ) &iso &iso (sym eq)
+       lemma1 (case2 eq) = subst₂ (λ j k → j ≡ k ) &iso &iso (sym eq)
 
-ω-prev-eq : {x y : Ordinal} →  od→ord (Union (ord→od y , (ord→od y , ord→od y))) ≡ od→ord (Union (ord→od x , (ord→od x , ord→od x))) → x ≡ y
+ω-prev-eq : {x y : Ordinal} →  & (Union (* y , (* y , * y))) ≡ & (Union (* x , (* x , * x))) → x ≡ y
 ω-prev-eq {x} {y} eq with trio< x y
 ω-prev-eq {x} {y} eq | tri< a ¬b ¬c = ⊥-elim (ω-prev-eq1 eq a)
 ω-prev-eq {x} {y} eq | tri≈ ¬a b ¬c = b
 ω-prev-eq {x} {y} eq | tri> ¬a ¬b c = ⊥-elim (ω-prev-eq1 (sym eq) c)
 
 ω-∈s : (x : HOD) →  Union ( x , (x , x)) ∋ x
-ω-∈s x not = not (od→ord (x , x)) record { proj1 = case2 refl ; proj2 = subst (λ k → odef k (od→ord x) ) (sym oiso) (case1 refl) }
+ω-∈s x not = not (& (x , x)) ⟪ case2 refl , subst (λ k → odef k (& x) ) (sym *iso) (case1 refl) ⟫
 
 ωs≠0 : (x : HOD) →  ¬ ( Union ( x , (x , x)) ≡ od∅ )
-ωs≠0 y eq =  ⊥-elim ( ¬x<0 (subst (λ k → od→ord y  o< k ) ord-od∅ (c<→o< (subst (λ k → odef k (od→ord y )) eq (ω-∈s y) ))) )
+ωs≠0 y eq =  ⊥-elim ( ¬x<0 (subst (λ k → & y  o< k ) ord-od∅ (c<→o< (subst (λ k → odef k (& y )) eq (ω-∈s y) ))) )
 
 nat→ω-iso : {i : HOD} → (lt : infinite ∋ i ) → nat→ω ( ω→nat i lt ) ≡ i
 nat→ω-iso {i} = ε-induction1 {λ i →  (lt : infinite ∋ i ) → nat→ω ( ω→nat i lt ) ≡ i  } ind i where
      ind : {x : HOD} → ({y : HOD} → x ∋ y → (lt : infinite ∋ y) → nat→ω (ω→nat y lt) ≡ y) →
                                             (lt : infinite ∋ x) → nat→ω (ω→nat x lt) ≡ x
-     ind {x} prev lt = ind1 lt oiso where
-         ind1 : {ox : Ordinal } → (ltd : infinite-d ox ) → ord→od ox ≡ x → nat→ω (ω→nato ltd) ≡ x
+     ind {x} prev lt = ind1 lt *iso where
+         ind1 : {ox : Ordinal } → (ltd : infinite-d ox ) → * ox ≡ x → nat→ω (ω→nato ltd) ≡ x
          ind1 {o∅} iφ refl = sym o∅≡od∅
          ind1 (isuc {x₁} ltd) ox=x = begin
               nat→ω (ω→nato (isuc ltd) )         
            ≡⟨⟩
               Union (nat→ω (ω→nato ltd) , (nat→ω (ω→nato ltd) , nat→ω (ω→nato ltd)))
            ≡⟨ cong (λ k → Union (k , (k , k ))) lemma  ⟩
-              Union (ord→od x₁ , (ord→od x₁ , ord→od x₁))
-           ≡⟨ trans ( sym oiso) ox=x ⟩
+              Union (* x₁ , (* x₁ , * x₁))
+           ≡⟨ trans ( sym *iso) ox=x ⟩
               x 
            ∎ where
                open ≡-Reasoning 
-               lemma0 :  x ∋ ord→od x₁
-               lemma0 = subst (λ k → odef k (od→ord (ord→od x₁))) (trans (sym oiso) ox=x) (λ not → not 
-                  (od→ord (ord→od x₁ , ord→od x₁))  record {proj1 = pair2 ; proj2 = subst (λ k → odef k (od→ord (ord→od x₁))) (sym oiso) pair1 } )
-               lemma1 : infinite ∋ ord→od x₁
-               lemma1 = subst (λ k → odef infinite k) (sym diso) ltd
+               lemma0 :  x ∋ * x₁
+               lemma0 = subst (λ k → odef k (& (* x₁))) (trans (sym *iso) ox=x) (λ not → not 
+                  (& (* x₁ , * x₁))  ⟪ pair2 , subst (λ k → odef k (& (* x₁))) (sym *iso) pair1 ⟫ )
+               lemma1 : infinite ∋ * x₁
+               lemma1 = subst (λ k → odef infinite k) (sym &iso) ltd
                lemma3 : {x y : Ordinal} → (ltd : infinite-d x ) (ltd1 : infinite-d y ) → y ≡ x → ltd ≅ ltd1
                lemma3 iφ iφ refl = HE.refl
-               lemma3 iφ (isuc {y} ltd1) eq = ⊥-elim ( ¬x<0 (subst₂ (λ j k → j o< k ) diso eq (c<→o< (ω-∈s (ord→od y)) )))
-               lemma3 (isuc {y} ltd)  iφ eq = ⊥-elim ( ¬x<0 (subst₂ (λ j k → j o< k ) diso (sym eq) (c<→o< (ω-∈s (ord→od y)) )))
+               lemma3 iφ (isuc {y} ltd1) eq = ⊥-elim ( ¬x<0 (subst₂ (λ j k → j o< k ) &iso eq (c<→o< (ω-∈s (* y)) )))
+               lemma3 (isuc {y} ltd)  iφ eq = ⊥-elim ( ¬x<0 (subst₂ (λ j k → j o< k ) &iso (sym eq) (c<→o< (ω-∈s (* y)) )))
                lemma3 (isuc {x} ltd) (isuc {y} ltd1) eq with lemma3 ltd ltd1 (ω-prev-eq (sym eq))
                ... | t = HE.cong₂ (λ j k → isuc {j} k ) (HE.≡-to-≅  (ω-prev-eq eq)) t  
                lemma2 : {x y : Ordinal} → (ltd : infinite-d x ) (ltd1 : infinite-d y ) → y ≡ x → ω→nato ltd ≡ ω→nato ltd1
                lemma2 {x} {y} ltd ltd1 eq = lemma6 eq (lemma3 {x} {y} ltd ltd1 eq)  where
                    lemma6 : {x y : Ordinal} → {ltd : infinite-d x } {ltd1 : infinite-d y } → y ≡ x → ltd ≅ ltd1 → ω→nato ltd ≡ ω→nato ltd1
                    lemma6 refl HE.refl = refl
-               lemma :  nat→ω (ω→nato ltd) ≡ ord→od x₁
-               lemma = trans  (cong (λ k →  nat→ω  k) (lemma2 {x₁} {_} ltd (subst (λ k → infinite-d k ) (sym diso) ltd)  diso ) ) ( prev {ord→od x₁} lemma0 lemma1 )
+               lemma :  nat→ω (ω→nato ltd) ≡ * x₁
+               lemma = trans  (cong (λ k →  nat→ω  k) (lemma2 {x₁} {_} ltd (subst (λ k → infinite-d k ) (sym &iso) ltd)  &iso ) ) ( prev {* x₁} lemma0 lemma1 )
 
 ω→nat-iso : {i : Nat} → ω→nat ( nat→ω i ) (ω∋nat→ω {i}) ≡ i
-ω→nat-iso {i} = lemma i (ω∋nat→ω {i}) oiso where
-   lemma : {x : Ordinal } → ( i : Nat ) → (ltd : infinite-d x ) → ord→od x ≡  nat→ω i → ω→nato ltd ≡ i
+ω→nat-iso {i} = lemma i (ω∋nat→ω {i}) *iso where
+   lemma : {x : Ordinal } → ( i : Nat ) → (ltd : infinite-d x ) → * x ≡  nat→ω i → ω→nato ltd ≡ i
    lemma {x} Zero iφ eq = refl
    lemma {x} (Suc i) iφ eq = ⊥-elim ( ωs≠0 (nat→ω i) (trans (sym eq) o∅≡od∅ )) -- Union (nat→ω i , (nat→ω i , nat→ω i)) ≡ od∅
-   lemma Zero (isuc {x} ltd) eq = ⊥-elim ( ωs≠0 (ord→od x) (subst (λ k → k ≡ od∅  ) oiso eq ))
-   lemma (Suc i) (isuc {x} ltd) eq = cong (λ k → Suc k ) (lemma i ltd (lemma1 eq) )  where -- ord→od x ≡ nat→ω i
-           lemma1 :  ord→od (od→ord (Union (ord→od x , (ord→od x , ord→od x)))) ≡ Union (nat→ω i , (nat→ω i , nat→ω i)) → ord→od x ≡ nat→ω i
-           lemma1 eq = subst (λ k → ord→od x ≡ k ) oiso (cong (λ k → ord→od k)
-                ( ω-prev-eq (subst (λ k → _ ≡ k ) diso (cong (λ k → od→ord k ) (sym
-                    (subst (λ k → _ ≡ Union ( k , ( k , k ))) (sym oiso ) eq ))))))
+   lemma Zero (isuc {x} ltd) eq = ⊥-elim ( ωs≠0 (* x) (subst (λ k → k ≡ od∅  ) *iso eq ))
+   lemma (Suc i) (isuc {x} ltd) eq = cong (λ k → Suc k ) (lemma i ltd (lemma1 eq) )  where -- * x ≡ nat→ω i
+           lemma1 :  * (& (Union (* x , (* x , * x)))) ≡ Union (nat→ω i , (nat→ω i , nat→ω i)) → * x ≡ nat→ω i
+           lemma1 eq = subst (λ k → * x ≡ k ) *iso (cong (λ k → * k)
+                ( ω-prev-eq (subst (λ k → _ ≡ k ) &iso (cong (λ k → & k ) (sym
+                    (subst (λ k → _ ≡ Union ( k , ( k , k ))) (sym *iso ) eq ))))))
 
 ψiso :  {ψ : HOD  → Set n} {x y : HOD } → ψ x → x ≡ y   → ψ y
 ψiso {ψ} t refl = t
 selection : {ψ : HOD → Set n} {X y : HOD} → ((X ∋ y) ∧ ψ y) ⇔ (Select X ψ ∋ y)
-selection {ψ} {X} {y} = record {
-    proj1 = λ cond → record { proj1 = proj1 cond ; proj2 = ψiso {ψ} (proj2 cond) (sym oiso)  }
-  ; proj2 = λ select → record { proj1 = proj1 select  ; proj2 =  ψiso {ψ} (proj2 select) oiso  }
-  }
+selection {ψ} {X} {y} = ⟪
+     ( λ cond → ⟪ proj1 cond , ψiso {ψ} (proj2 cond) (sym *iso)  ⟫ )
+  ,  ( λ select → ⟪ proj1 select  , ψiso {ψ} (proj2 select) *iso  ⟫ )
+  ⟫
 
 selection-in-domain : {ψ : HOD → Set n} {X y : HOD} → Select X ψ ∋ y → X ∋ y 
 selection-in-domain {ψ} {X} {y} lt = proj1 ((proj2 (selection {ψ} {X} )) lt)
 
-sup-c< :  (ψ : HOD → HOD) → {X x : HOD} → X ∋ x  → od→ord (ψ x) o< (sup-o X (λ y X∋y → od→ord (ψ (ord→od y))))
-sup-c< ψ {X} {x} lt = subst (λ k → od→ord (ψ k) o< _ ) oiso (sup-o< X lt )
+sup-c< :  (ψ : HOD → HOD) → {X x : HOD} → X ∋ x  → & (ψ x) o< (sup-o X (λ y X∋y → & (ψ (* y))))
+sup-c< ψ {X} {x} lt = subst (λ k → & (ψ k) o< _ ) *iso (sup-o< X lt )
 replacement← : {ψ : HOD → HOD} (X x : HOD) →  X ∋ x → Replace X ψ ∋ ψ x
-replacement← {ψ} X x lt = record { proj1 =  sup-c< ψ {X} {x} lt ; proj2 = lemma } where 
-    lemma : def (in-codomain X ψ) (od→ord (ψ x))
-    lemma not = ⊥-elim ( not ( od→ord x ) (record { proj1 = lt ; proj2 = cong (λ k → od→ord (ψ k)) (sym oiso)} ))
+replacement← {ψ} X x lt = ⟪ sup-c< ψ {X} {x} lt , lemma ⟫ where 
+    lemma : def (in-codomain X ψ) (& (ψ x))
+    lemma not = ⊥-elim ( not ( & x ) (⟪ lt , cong (λ k → & (ψ k)) (sym *iso)⟫ ))
 replacement→ : {ψ : HOD → HOD} (X x : HOD) → (lt : Replace X ψ ∋ x) → ¬ ( (y : HOD) → ¬ (x =h= ψ y))
 replacement→ {ψ} X x lt = contra-position lemma (lemma2 (proj2 lt)) where
-    lemma2 :  ¬ ((y : Ordinal) → ¬ odef X y ∧ ((od→ord x) ≡ od→ord (ψ (ord→od y))))
-            → ¬ ((y : Ordinal) → ¬ odef X y ∧ (ord→od (od→ord x) =h= ψ (ord→od y)))
-    lemma2 not not2  = not ( λ y d →  not2 y (record { proj1 = proj1 d ; proj2 = lemma3 (proj2 d)})) where
-        lemma3 : {y : Ordinal } → (od→ord x ≡ od→ord (ψ (ord→od  y))) → (ord→od (od→ord x) =h= ψ (ord→od y))  
-        lemma3 {y} eq = subst (λ k  → ord→od (od→ord x) =h= k ) oiso (o≡→== eq )
-    lemma :  ( (y : HOD) → ¬ (x =h= ψ y)) → ( (y : Ordinal) → ¬ odef X y ∧ (ord→od (od→ord x) =h= ψ (ord→od y)) )
-    lemma not y not2 = not (ord→od y) (subst (λ k → k =h= ψ (ord→od y)) oiso  ( proj2 not2 ))
+    lemma2 :  ¬ ((y : Ordinal) → ¬ odef X y ∧ ((& x) ≡ & (ψ (* y))))
+            → ¬ ((y : Ordinal) → ¬ odef X y ∧ (* (& x) =h= ψ (* y)))
+    lemma2 not not2  = not ( λ y d →  not2 y (⟪ proj1 d , lemma3 (proj2 d)⟫)) where
+        lemma3 : {y : Ordinal } → (& x ≡ & (ψ (*  y))) → (* (& x) =h= ψ (* y))  
+        lemma3 {y} eq = subst (λ k  → * (& x) =h= k ) *iso (o≡→== eq )
+    lemma :  ( (y : HOD) → ¬ (x =h= ψ y)) → ( (y : Ordinal) → ¬ odef X y ∧ (* (& x) =h= ψ (* y)) )
+    lemma not y not2 = not (* y) (subst (λ k → k =h= ψ (* y)) *iso  ( proj2 not2 ))
 
 ---
 --- Power Set
@@ -609,126 +609,123 @@
 --
 ∩-≡ :  { a b : HOD  } → ({x : HOD  } → (a ∋ x → b ∋ x)) → a =h= ( b ∩ a )
 ∩-≡ {a} {b} inc = record {
-   eq→ = λ {x} x<a → record { proj2 = x<a ;
-        proj1 = odef-subst  {_} {_} {b} {x} (inc (d→∋ a x<a)) refl diso  } ;
+   eq→ = λ {x} x<a → ⟪ odef-subst  {_} {_} {b} {x} (inc (d→∋ a x<a)) refl &iso , x<a  ⟫ ;
    eq← = λ {x} x<a∩b → proj2 x<a∩b }
 -- 
 -- Transitive Set case
 -- we have t ∋ x → Ord a ∋ x means t is a subset of Ord a, that is (Ord a) ∩ t =h= t
 -- OPwr (Ord a) is a sup of (Ord a) ∩ t, so OPwr (Ord a) ∋ t
--- OPwr  A = Ord ( sup-o ( λ x → od→ord ( A ∩ (ord→od x )) ) )   
+-- OPwr  A = Ord ( sup-o ( λ x → & ( A ∩ (* x )) ) )   
 -- 
 ord-power← : (a : Ordinal ) (t : HOD) → ({x : HOD} → (t ∋ x → (Ord a) ∋ x)) → OPwr (Ord a) ∋ t
-ord-power← a t t→A  = odef-subst  {_} {_} {OPwr (Ord a)} {od→ord t}
+ord-power← a t t→A  = odef-subst  {_} {_} {OPwr (Ord a)} {& t}
         lemma refl (lemma1 lemma-eq )where
     lemma-eq :  ((Ord a) ∩ t) =h= t
     eq→ lemma-eq {z} w = proj2 w 
-    eq← lemma-eq {z} w = record { proj2 = w  ;
-        proj1 = odef-subst  {_} {_} {(Ord a)} {z}
-        ( t→A (d→∋ t w)) refl diso  }
+    eq← lemma-eq {z} w = ⟪ odef-subst  {_} {_} {(Ord a)} {z} ( t→A (d→∋ t w)) refl &iso  , w ⟫
     lemma1 :  {a : Ordinal } { t : HOD }
-        → (eq : ((Ord a) ∩ t) =h= t)  → od→ord ((Ord a) ∩ (ord→od (od→ord t))) ≡ od→ord t
-    lemma1  {a} {t} eq = subst (λ k → od→ord ((Ord a) ∩ k) ≡ od→ord t ) (sym oiso) (cong (λ k → od→ord k ) (==→o≡ eq ))
-    lemma2 : (od→ord t) o< (osuc (od→ord (Ord a)))
-    lemma2 = ⊆→o≤  {t} {Ord a} (λ {x} x<t → subst (λ k → def (od (Ord a)) k) diso (t→A (d→∋ t x<t))) 
-    lemma :  od→ord ((Ord a) ∩ (ord→od (od→ord t)) ) o< sup-o (Ord (osuc (od→ord (Ord a)))) (λ x lt → od→ord ((Ord a) ∩ (ord→od x)))
+        → (eq : ((Ord a) ∩ t) =h= t)  → & ((Ord a) ∩ (* (& t))) ≡ & t
+    lemma1  {a} {t} eq = subst (λ k → & ((Ord a) ∩ k) ≡ & t ) (sym *iso) (cong (λ k → & k ) (==→o≡ eq ))
+    lemma2 : (& t) o< (osuc (& (Ord a)))
+    lemma2 = ⊆→o≤  {t} {Ord a} (λ {x} x<t → subst (λ k → def (od (Ord a)) k) &iso (t→A (d→∋ t x<t))) 
+    lemma :  & ((Ord a) ∩ (* (& t)) ) o< sup-o (Ord (osuc (& (Ord a)))) (λ x lt → & ((Ord a) ∩ (* x)))
     lemma = sup-o< _ lemma2
 
 -- 
--- Every set in HOD is a subset of Ordinals, so make OPwr (Ord (od→ord A)) first
+-- Every set in HOD is a subset of Ordinals, so make OPwr (Ord (& A)) first
 -- then replace of all elements of the Power set by A ∩ y
 -- 
--- Power A = Replace (OPwr (Ord (od→ord A))) ( λ y → A ∩ y )
+-- Power A = Replace (OPwr (Ord (& A))) ( λ y → A ∩ y )
 
 -- we have oly double negation form because of the replacement axiom
 --
 power→ :  ( A t : HOD) → Power A ∋ t → {x : HOD} → t ∋ x → ¬ ¬ (A ∋ x)
 power→ A t P∋t {x} t∋x = FExists _ lemma5 lemma4 where
-    a = od→ord A
+    a = & A
     lemma2 : ¬ ( (y : HOD) → ¬ (t =h=  (A ∩ y)))
-    lemma2 = replacement→ {λ x → A ∩ x} (OPwr (Ord (od→ord A))) t P∋t
+    lemma2 = replacement→ {λ x → A ∩ x} (OPwr (Ord (& A))) t P∋t
     lemma3 : (y : HOD) → t =h= ( A ∩ y ) → ¬ ¬ (A ∋ x)
     lemma3 y eq not = not (proj1 (eq→ eq t∋x))
-    lemma4 : ¬ ((y : Ordinal) → ¬ (t =h= (A ∩ ord→od y)))
-    lemma4 not = lemma2 ( λ y not1 → not (od→ord y) (subst (λ k → t =h= ( A ∩ k )) (sym oiso) not1 ))
-    lemma5 : {y : Ordinal} → t =h= (A ∩ ord→od y) →  ¬ ¬  (odef A (od→ord x))
-    lemma5 {y} eq not = (lemma3 (ord→od y) eq) not
+    lemma4 : ¬ ((y : Ordinal) → ¬ (t =h= (A ∩ * y)))
+    lemma4 not = lemma2 ( λ y not1 → not (& y) (subst (λ k → t =h= ( A ∩ k )) (sym *iso) not1 ))
+    lemma5 : {y : Ordinal} → t =h= (A ∩ * y) →  ¬ ¬  (odef A (& x))
+    lemma5 {y} eq not = (lemma3 (* y) eq) not
 
 power← :  (A t : HOD) → ({x : HOD} → (t ∋ x → A ∋ x)) → Power A ∋ t
-power← A t t→A = record { proj1 = lemma1 ; proj2 = lemma2 } where 
-    a = od→ord A
+power← A t t→A = ⟪ lemma1 , lemma2 ⟫ where 
+    a = & A
     lemma0 : {x : HOD} → t ∋ x → Ord a ∋ x
     lemma0 {x} t∋x = c<→o< (t→A t∋x)
     lemma3 : OPwr (Ord a) ∋ t
     lemma3 = ord-power← a t lemma0
-    lemma4 :  (A ∩ ord→od (od→ord t)) ≡ t
+    lemma4 :  (A ∩ * (& t)) ≡ t
     lemma4 = let open ≡-Reasoning in begin
-        A ∩ ord→od (od→ord t)
-        ≡⟨ cong (λ k → A ∩ k) oiso ⟩
+        A ∩ * (& t)
+        ≡⟨ cong (λ k → A ∩ k) *iso ⟩
         A ∩ t
         ≡⟨ sym (==→o≡ ( ∩-≡ {t} {A} t→A )) ⟩
         t
         ∎
     sup1 : Ordinal
-    sup1 =  sup-o (Ord (osuc (od→ord (Ord (od→ord A))))) (λ x A∋x → od→ord ((Ord (od→ord A)) ∩ (ord→od x)))
-    lemma9 : def (od (Ord (Ordinals.osuc O (od→ord (Ord (od→ord A)))))) (od→ord (Ord (od→ord A)))
+    sup1 =  sup-o (Ord (osuc (& (Ord (& A))))) (λ x A∋x → & ((Ord (& A)) ∩ (* x)))
+    lemma9 : def (od (Ord (Ordinals.osuc O (& (Ord (& A)))))) (& (Ord (& A)))
     lemma9 = <-osuc 
-    lemmab : od→ord ((Ord (od→ord A)) ∩ (ord→od (od→ord (Ord (od→ord A) )))) o< sup1
-    lemmab = sup-o< (Ord (osuc (od→ord (Ord (od→ord A))))) lemma9 
-    lemmad : Ord (osuc (od→ord A)) ∋ t
-    lemmad = ⊆→o≤ (λ {x} lt → subst (λ k → def (od A) k ) diso (t→A (d→∋ t lt))) 
-    lemmac : ((Ord (od→ord A)) ∩  (ord→od (od→ord (Ord (od→ord A) )))) =h= Ord (od→ord A)
+    lemmab : & ((Ord (& A)) ∩ (* (& (Ord (& A) )))) o< sup1
+    lemmab = sup-o< (Ord (osuc (& (Ord (& A))))) lemma9 
+    lemmad : Ord (osuc (& A)) ∋ t
+    lemmad = ⊆→o≤ (λ {x} lt → subst (λ k → def (od A) k ) &iso (t→A (d→∋ t lt))) 
+    lemmac : ((Ord (& A)) ∩  (* (& (Ord (& A) )))) =h= Ord (& A)
     lemmac = record { eq→ = lemmaf ; eq← = lemmag } where
-        lemmaf : {x : Ordinal} → def (od ((Ord (od→ord A)) ∩  (ord→od (od→ord (Ord (od→ord A)))))) x → def (od (Ord (od→ord A))) x
+        lemmaf : {x : Ordinal} → def (od ((Ord (& A)) ∩  (* (& (Ord (& A)))))) x → def (od (Ord (& A))) x
         lemmaf {x} lt = proj1 lt
-        lemmag :  {x : Ordinal} → def (od (Ord (od→ord A))) x → def (od ((Ord (od→ord A)) ∩ (ord→od (od→ord (Ord (od→ord A)))))) x
-        lemmag {x} lt = record { proj1 = lt ; proj2 = subst (λ k → def (od k) x) (sym oiso) lt } 
-    lemmae : od→ord ((Ord (od→ord A)) ∩ (ord→od (od→ord (Ord (od→ord A))))) ≡ od→ord (Ord (od→ord A))
-    lemmae = cong (λ k → od→ord k ) ( ==→o≡ lemmac)
-    lemma7 : def (od (OPwr (Ord (od→ord A)))) (od→ord t)
+        lemmag :  {x : Ordinal} → def (od (Ord (& A))) x → def (od ((Ord (& A)) ∩ (* (& (Ord (& A)))))) x
+        lemmag {x} lt = ⟪ lt , subst (λ k → def (od k) x) (sym *iso) lt ⟫ 
+    lemmae : & ((Ord (& A)) ∩ (* (& (Ord (& A))))) ≡ & (Ord (& A))
+    lemmae = cong (λ k → & k ) ( ==→o≡ lemmac)
+    lemma7 : def (od (OPwr (Ord (& A)))) (& t)
     lemma7 with osuc-≡< lemmad
     lemma7 | case2 lt = ordtrans (c<→o< lt) (subst (λ k → k o< sup1) lemmae lemmab )
-    lemma7 | case1 eq with osuc-≡< (⊆→o≤ {ord→od (od→ord t)} {ord→od (od→ord (Ord (od→ord t)))} (λ {x} lt → lemmah lt )) where
-        lemmah : {x : Ordinal } → def (od (ord→od (od→ord t))) x → def (od (ord→od (od→ord (Ord (od→ord t))))) x
-        lemmah {x} lt = subst (λ k → def (od k) x ) (sym oiso) (subst (λ k → k o< (od→ord t))
-            diso
-            (c<→o< (subst₂ (λ j k → def (od j)  k) oiso (sym diso) lt )))
+    lemma7 | case1 eq with osuc-≡< (⊆→o≤ {* (& t)} {* (& (Ord (& t)))} (λ {x} lt → lemmah lt )) where
+        lemmah : {x : Ordinal } → def (od (* (& t))) x → def (od (* (& (Ord (& t))))) x
+        lemmah {x} lt = subst (λ k → def (od k) x ) (sym *iso) (subst (λ k → k o< (& t))
+            &iso
+            (c<→o< (subst₂ (λ j k → def (od j)  k) *iso (sym &iso) lt )))
     lemma7 | case1 eq | case1 eq1 = subst (λ k → k o< sup1) (trans lemmae lemmai) lemmab where 
-        lemmai : od→ord (Ord (od→ord A)) ≡ od→ord t
+        lemmai : & (Ord (& A)) ≡ & t
         lemmai = let open ≡-Reasoning in begin
-                od→ord (Ord (od→ord A)) 
-            ≡⟨ sym (cong (λ k → od→ord (Ord k)) eq) ⟩
-                od→ord (Ord (od→ord t)) 
-            ≡⟨ sym diso ⟩
-                od→ord (ord→od (od→ord (Ord (od→ord t))))
+                & (Ord (& A)) 
+            ≡⟨ sym (cong (λ k → & (Ord k)) eq) ⟩
+                & (Ord (& t)) 
+            ≡⟨ sym &iso ⟩
+                & (* (& (Ord (& t))))
             ≡⟨ sym eq1 ⟩
-                od→ord (ord→od (od→ord t))
-            ≡⟨ diso ⟩
-                od→ord t 
+                & (* (& t))
+            ≡⟨ &iso ⟩
+                & t 
             ∎
     lemma7 | case1 eq | case2 lt = ordtrans lemmaj (subst (λ k → k o< sup1) lemmae lemmab ) where
-        lemmak : od→ord (ord→od (od→ord (Ord (od→ord t)))) ≡ od→ord (Ord (od→ord A))
+        lemmak : & (* (& (Ord (& t)))) ≡ & (Ord (& A))
         lemmak = let open ≡-Reasoning in begin
-                od→ord (ord→od (od→ord (Ord (od→ord t))))
-            ≡⟨ diso ⟩
-                od→ord (Ord (od→ord t))
-            ≡⟨ cong (λ k → od→ord (Ord k)) eq ⟩
-                od→ord (Ord (od→ord A))
+                & (* (& (Ord (& t))))
+            ≡⟨ &iso ⟩
+                & (Ord (& t))
+            ≡⟨ cong (λ k → & (Ord k)) eq ⟩
+                & (Ord (& A))
             ∎
-        lemmaj : od→ord t o< od→ord (Ord (od→ord A))
-        lemmaj = subst₂ (λ j k → j o< k ) diso lemmak lt 
-    lemma1 : od→ord t o< sup-o (OPwr (Ord (od→ord A))) (λ x lt → od→ord (A ∩ (ord→od x)))
-    lemma1 = subst (λ k → od→ord k o< sup-o (OPwr (Ord (od→ord A)))  (λ x lt → od→ord (A ∩ (ord→od x))))
-        lemma4 (sup-o< (OPwr (Ord (od→ord A))) lemma7 )
-    lemma2 :  def (in-codomain (OPwr (Ord (od→ord A))) (_∩_ A)) (od→ord t)
-    lemma2 not = ⊥-elim ( not (od→ord t) (record { proj1 = lemma3 ; proj2 = lemma6 }) ) where
-        lemma6 : od→ord t ≡ od→ord (A ∩ ord→od (od→ord t)) 
-        lemma6 = cong ( λ k → od→ord k ) (==→o≡ (subst (λ k → t =h= (A ∩ k)) (sym oiso) ( ∩-≡ {t} {A} t→A  )))
+        lemmaj : & t o< & (Ord (& A))
+        lemmaj = subst₂ (λ j k → j o< k ) &iso lemmak lt 
+    lemma1 : & t o< sup-o (OPwr (Ord (& A))) (λ x lt → & (A ∩ (* x)))
+    lemma1 = subst (λ k → & k o< sup-o (OPwr (Ord (& A)))  (λ x lt → & (A ∩ (* x))))
+        lemma4 (sup-o< (OPwr (Ord (& A))) lemma7 )
+    lemma2 :  def (in-codomain (OPwr (Ord (& A))) (_∩_ A)) (& t)
+    lemma2 not = ⊥-elim ( not (& t) (⟪ lemma3 , lemma6 ⟫) ) where
+        lemma6 : & t ≡ & (A ∩ * (& t)) 
+        lemma6 = cong ( λ k → & k ) (==→o≡ (subst (λ k → t =h= (A ∩ k)) (sym *iso) ( ∩-≡ {t} {A} t→A  )))
 
 
 ord⊆power : (a : Ordinal) → (Ord (osuc a)) ⊆ (Power (Ord a)) 
 ord⊆power a = record { incl = λ {x} lt →  power← (Ord a) x (lemma lt) } where
-    lemma : {x y : HOD} → od→ord x o< osuc a → x ∋ y →  Ord a ∋ y
+    lemma : {x y : HOD} → & x o< osuc a → x ∋ y →  Ord a ∋ y
     lemma lt y<x with osuc-≡< lt
     lemma lt y<x | case1 refl = c<→o< y<x
     lemma lt y<x | case2 x<a = ordtrans (c<→o< y<x) x<a 
@@ -737,28 +734,28 @@
 continuum-hyphotheis a = Power (Ord a) ⊆ Ord (osuc a)
 
 extensionality0 : {A B : HOD } → ((z : HOD) → (A ∋ z) ⇔ (B ∋ z)) → A =h= B
-eq→ (extensionality0 {A} {B} eq ) {x} d = odef-iso  {A} {B} (sym diso) (proj1 (eq (ord→od x))) d  
-eq← (extensionality0 {A} {B} eq ) {x} d = odef-iso  {B} {A} (sym diso) (proj2 (eq (ord→od x))) d  
+eq→ (extensionality0 {A} {B} eq ) {x} d = odef-iso  {A} {B} (sym &iso) (proj1 (eq (* x))) d  
+eq← (extensionality0 {A} {B} eq ) {x} d = odef-iso  {B} {A} (sym &iso) (proj2 (eq (* x))) d  
 
 extensionality : {A B w : HOD  } → ((z : HOD ) → (A ∋ z) ⇔ (B ∋ z)) → (w ∋ A) ⇔ (w ∋ B)
 proj1 (extensionality {A} {B} {w} eq ) d = subst (λ k → w ∋ k) ( ==→o≡ (extensionality0 {A} {B} eq) ) d
 proj2 (extensionality {A} {B} {w} eq ) d = subst (λ k → w ∋ k) (sym ( ==→o≡ (extensionality0 {A} {B} eq) )) d 
 
 infinity∅ : infinite  ∋ od∅ 
-infinity∅ = odef-subst  {_} {_} {infinite} {od→ord (od∅ )} iφ refl lemma where
-    lemma : o∅ ≡ od→ord od∅
+infinity∅ = odef-subst  {_} {_} {infinite} {& (od∅ )} iφ refl lemma where
+    lemma : o∅ ≡ & od∅
     lemma =  let open ≡-Reasoning in begin
         o∅
-        ≡⟨ sym diso ⟩
-        od→ord ( ord→od o∅ )
-        ≡⟨ cong ( λ k → od→ord k ) o∅≡od∅ ⟩
-        od→ord od∅
+        ≡⟨ sym &iso ⟩
+        & ( * o∅ )
+        ≡⟨ cong ( λ k → & k ) o∅≡od∅ ⟩
+        & od∅
         ∎
 infinity : (x : HOD) → infinite ∋ x → infinite ∋ Union (x , (x , x ))
-infinity x lt = odef-subst  {_} {_} {infinite} {od→ord (Union (x , (x , x )))} ( isuc {od→ord x} lt ) refl lemma where
-    lemma :  od→ord (Union (ord→od (od→ord x) , (ord→od (od→ord x) , ord→od (od→ord x))))
-        ≡ od→ord (Union (x , (x , x)))
-    lemma = cong (λ k → od→ord (Union ( k , ( k , k ) ))) oiso 
+infinity x lt = odef-subst  {_} {_} {infinite} {& (Union (x , (x , x )))} ( isuc {& x} lt ) refl lemma where
+    lemma :  & (Union (* (& x) , (* (& x) , * (& x))))
+        ≡ & (Union (x , (x , x)))
+    lemma = cong (λ k → & (Union ( k , ( k , k ) ))) *iso 
 
 isZF : IsZF (HOD )  _∋_  _=h=_ od∅ _,_ Union Power Select Replace infinite
 isZF = record {
diff -r cb067605fea0 -r 44a484f17f26 ODC.agda
--- a/ODC.agda	Fri Jul 31 17:54:52 2020 +0900
+++ b/ODC.agda	Sat Aug 01 11:06:29 2020 +0900
@@ -30,9 +30,9 @@
   -- mimimul and x∋minimal is an Axiom of choice
   minimal : (x : HOD  ) → ¬ (x =h= od∅ )→ HOD 
   -- this should be ¬ (x =h= od∅ )→ ∃ ox → x ∋ Ord ox  ( minimum of x )
-  x∋minimal : (x : HOD  ) → ( ne : ¬ (x =h= od∅ ) ) → odef x ( od→ord ( minimal x ne ) )
+  x∋minimal : (x : HOD  ) → ( ne : ¬ (x =h= od∅ ) ) → odef x ( & ( minimal x ne ) )
   -- minimality (may proved by ε-induction with LEM)
-  minimal-1 : (x : HOD  ) → ( ne : ¬ (x =h= od∅ ) ) → (y : HOD ) → ¬ ( odef (minimal x ne) (od→ord y)) ∧ (odef x (od→ord  y) )
+  minimal-1 : (x : HOD  ) → ( ne : ¬ (x =h= od∅ ) ) → (y : HOD ) → ¬ ( odef (minimal x ne) (& y)) ∧ (odef x (&  y) )
 
 
 --
@@ -48,19 +48,19 @@
 ppp  {p} {a} d = proj2 d
 
 p∨¬p : ( p : Set n ) → p ∨ ( ¬ p )         -- assuming axiom of choice
-p∨¬p  p with is-o∅ ( od→ord (pred-od p ))
+p∨¬p  p with is-o∅ ( & (pred-od p ))
 p∨¬p  p | yes eq = case2 (¬p eq) where
    ps = pred-od p 
-   eqo∅ : ps =h=  od∅  → od→ord ps ≡  o∅  
-   eqo∅ eq = subst (λ k → od→ord ps ≡ k) ord-od∅ ( cong (λ k → od→ord k ) (==→o≡ eq)) 
+   eqo∅ : ps =h=  od∅  → & ps ≡  o∅  
+   eqo∅ eq = subst (λ k → & ps ≡ k) ord-od∅ ( cong (λ k → & k ) (==→o≡ eq)) 
    lemma : ps =h= od∅ → p → ⊥
-   lemma eq p0 = ¬x<0  {od→ord ps} (eq→ eq record { proj1 = eqo∅ eq ; proj2 = p0 } )
-   ¬p : (od→ord ps ≡ o∅) → p → ⊥
-   ¬p eq = lemma ( subst₂ (λ j k → j =h=  k ) oiso o∅≡od∅ ( o≡→== eq ))
+   lemma eq p0 = ¬x<0  {& ps} (eq→ eq record { proj1 = eqo∅ eq ; proj2 = p0 } )
+   ¬p : (& ps ≡ o∅) → p → ⊥
+   ¬p eq = lemma ( subst₂ (λ j k → j =h=  k ) *iso o∅≡od∅ ( o≡→== eq ))
 p∨¬p  p | no ¬p = case1 (ppp  {p} {minimal ps (λ eq →  ¬p (eqo∅ eq))} lemma) where
    ps = pred-od p 
-   eqo∅ : ps =h=  od∅  → od→ord ps ≡  o∅  
-   eqo∅ eq = subst (λ k → od→ord ps ≡ k) ord-od∅ ( cong (λ k → od→ord k ) (==→o≡ eq)) 
+   eqo∅ : ps =h=  od∅  → & ps ≡  o∅  
+   eqo∅ eq = subst (λ k → & ps ≡ k) ord-od∅ ( cong (λ k → & k ) (==→o≡ eq)) 
    lemma : ps ∋ minimal ps (λ eq →  ¬p (eqo∅ eq)) 
    lemma = x∋minimal ps (λ eq →  ¬p (eqo∅ eq))
 
@@ -87,7 +87,7 @@
    t1 = power→ A t PA∋t
 
 OrdP : ( x : Ordinal  ) ( y : HOD  ) → Dec ( Ord x ∋ y )
-OrdP  x y with trio< x (od→ord y)
+OrdP  x y with trio< x (& y)
 OrdP  x y | tri< a ¬b ¬c = no ¬c
 OrdP  x y | tri≈ ¬a refl ¬c = no ( o<¬≡ refl )
 OrdP  x y | tri> ¬a ¬b c = yes c
diff -r cb067605fea0 -r 44a484f17f26 OPair.agda
--- a/OPair.agda	Fri Jul 31 17:54:52 2020 +0900
+++ b/OPair.agda	Sat Aug 01 11:06:29 2020 +0900
@@ -40,56 +40,56 @@
     right (case1 t) = case2 t
     right (case2 t) = case1 t
 
-ord≡→≡ : { x y : HOD } → od→ord x ≡ od→ord y → x ≡ y
-ord≡→≡ eq = subst₂ (λ j k → j ≡ k ) oiso oiso ( cong ( λ k → ord→od k ) eq )
+ord≡→≡ : { x y : HOD } → & x ≡ & y → x ≡ y
+ord≡→≡ eq = subst₂ (λ j k → j ≡ k ) *iso *iso ( cong ( λ k → * k ) eq )
 
-od≡→≡ : { x y : Ordinal } → ord→od x ≡ ord→od y → x ≡ y
-od≡→≡ eq = subst₂ (λ j k → j ≡ k ) diso diso ( cong ( λ k → od→ord k ) eq )
+od≡→≡ : { x y : Ordinal } → * x ≡ * y → x ≡ y
+od≡→≡ eq = subst₂ (λ j k → j ≡ k ) &iso &iso ( cong ( λ k → & k ) eq )
 
 eq-prod : { x x' y y' : HOD } → x ≡ x' → y ≡ y' → < x , y > ≡ < x' , y' >
 eq-prod refl refl = refl
 
 xx=zy→x=y : {x y z : HOD } → ( x , x ) =h= ( z , y ) → x ≡ y
-xx=zy→x=y {x} {y} eq with trio< (od→ord x) (od→ord y) 
-xx=zy→x=y {x} {y} eq | tri< a ¬b ¬c with eq← eq {od→ord y} (case2 refl) 
+xx=zy→x=y {x} {y} eq with trio< (& x) (& y) 
+xx=zy→x=y {x} {y} eq | tri< a ¬b ¬c with eq← eq {& y} (case2 refl) 
 xx=zy→x=y {x} {y} eq | tri< a ¬b ¬c | case1 s = ⊥-elim ( o<¬≡ (sym s) a )
 xx=zy→x=y {x} {y} eq | tri< a ¬b ¬c | case2 s = ⊥-elim ( o<¬≡ (sym s) a )
 xx=zy→x=y {x} {y} eq | tri≈ ¬a b ¬c = ord≡→≡ b
-xx=zy→x=y {x} {y} eq | tri> ¬a ¬b c  with eq← eq {od→ord y} (case2 refl) 
+xx=zy→x=y {x} {y} eq | tri> ¬a ¬b c  with eq← eq {& y} (case2 refl) 
 xx=zy→x=y {x} {y} eq | tri> ¬a ¬b c | case1 s = ⊥-elim ( o<¬≡ s c )
 xx=zy→x=y {x} {y} eq | tri> ¬a ¬b c | case2 s = ⊥-elim ( o<¬≡ s c )
 
 prod-eq : { x x' y y' : HOD } → < x , y > =h= < x' , y' > → (x ≡ x' ) ∧ ( y ≡ y' )
-prod-eq {x} {x'} {y} {y'} eq = record { proj1 = lemmax ; proj2 = lemmay } where
+prod-eq {x} {x'} {y} {y'} eq = ⟪ lemmax , lemmay ⟫ where
     lemma2 : {x y z : HOD } → ( x , x ) =h= ( z , y ) → z ≡ y
     lemma2 {x} {y} {z} eq = trans (sym (xx=zy→x=y lemma3 )) ( xx=zy→x=y eq )  where
         lemma3 : ( x , x ) =h= ( y , z )
         lemma3 = ==-trans eq exg-pair
     lemma1 : {x y : HOD } → ( x , x ) =h= ( y , y ) → x ≡ y
-    lemma1 {x} {y} eq with eq← eq {od→ord y} (case2 refl)
+    lemma1 {x} {y} eq with eq← eq {& y} (case2 refl)
     lemma1 {x} {y} eq | case1 s = ord≡→≡ (sym s)
     lemma1 {x} {y} eq | case2 s = ord≡→≡ (sym s)
     lemma4 : {x y z : HOD } → ( x , y ) =h= ( x , z ) → y ≡ z
-    lemma4 {x} {y} {z} eq with eq← eq {od→ord z} (case2 refl)
+    lemma4 {x} {y} {z} eq with eq← eq {& z} (case2 refl)
     lemma4 {x} {y} {z} eq | case1 s with ord≡→≡ s -- x ≡ z
     ... | refl with lemma2 (==-sym eq )
     ... | refl = refl
     lemma4 {x} {y} {z} eq | case2 s = ord≡→≡ (sym s) -- y ≡ z
     lemmax : x ≡ x'
-    lemmax with eq→ eq {od→ord (x , x)} (case1 refl) 
+    lemmax with eq→ eq {& (x , x)} (case1 refl) 
     lemmax | case1 s = lemma1 (ord→== s )  -- (x,x)≡(x',x')
     lemmax | case2 s with lemma2 (ord→== s ) -- (x,x)≡(x',y') with x'≡y'
     ... | refl = lemma1 (ord→== s )
     lemmay : y ≡ y'
     lemmay with lemmax
     ... | refl with lemma4 eq -- with (x,y)≡(x,y')
-    ... | eq1 = lemma4 (ord→== (cong (λ  k → od→ord k )  eq1 ))
+    ... | eq1 = lemma4 (ord→== (cong (λ  k → & k )  eq1 ))
 
 --
 -- unlike ordered pair, ZFProduct is not a HOD
 
 data ord-pair : (p : Ordinal) → Set n where
-   pair : (x y : Ordinal ) → ord-pair ( od→ord ( < ord→od x , ord→od y > ) )
+   pair : (x y : Ordinal ) → ord-pair ( & ( < * x , * y > ) )
 
 ZFProduct : OD
 ZFProduct = record { def = λ x → ord-pair x }
@@ -101,55 +101,55 @@
 pi1 : { p : Ordinal } →   ord-pair p →  Ordinal
 pi1 ( pair x y) = x
 
-π1 : { p : HOD } → def ZFProduct (od→ord p) → HOD
-π1 lt = ord→od (pi1 lt )
+π1 : { p : HOD } → def ZFProduct (& p) → HOD
+π1 lt = * (pi1 lt )
 
 pi2 : { p : Ordinal } →   ord-pair p →  Ordinal
 pi2 ( pair x y ) = y
 
-π2 : { p : HOD } → def ZFProduct (od→ord p) → HOD
-π2 lt = ord→od (pi2 lt )
+π2 : { p : HOD } → def ZFProduct (& p) → HOD
+π2 lt = * (pi2 lt )
 
-op-cons :  { ox oy  : Ordinal } → def ZFProduct (od→ord ( < ord→od ox , ord→od oy >   ))
+op-cons :  { ox oy  : Ordinal } → def ZFProduct (& ( < * ox , * oy >   ))
 op-cons {ox} {oy} = pair ox oy
 
 def-subst :  {Z : OD } {X : Ordinal  }{z : OD } {x : Ordinal  }→ def Z X → Z ≡ z  →  X ≡ x  →  def z x
 def-subst df refl refl = df
 
-p-cons :  ( x y  : HOD ) → def ZFProduct (od→ord ( < x , y >))
-p-cons x y = def-subst {_} {_} {ZFProduct} {od→ord (< x , y >)} (pair (od→ord x) ( od→ord y )) refl (
+p-cons :  ( x y  : HOD ) → def ZFProduct (& ( < x , y >))
+p-cons x y = def-subst {_} {_} {ZFProduct} {& (< x , y >)} (pair (& x) ( & y )) refl (
    let open ≡-Reasoning in begin
-       od→ord < ord→od (od→ord x) , ord→od (od→ord y) >
-   ≡⟨ cong₂ (λ j k → od→ord < j , k >) oiso oiso ⟩
-       od→ord < x , y >
+       & < * (& x) , * (& y) >
+   ≡⟨ cong₂ (λ j k → & < j , k >) *iso *iso ⟩
+       & < x , y >
    ∎ ) 
 
-op-iso :  { op : Ordinal } → (q : ord-pair op ) → od→ord < ord→od (pi1 q) , ord→od (pi2 q) > ≡ op
+op-iso :  { op : Ordinal } → (q : ord-pair op ) → & < * (pi1 q) , * (pi2 q) > ≡ op
 op-iso (pair ox oy) = refl
 
-p-iso :  { x  : HOD } → (p : def ZFProduct (od→ord  x) ) → < π1 p , π2 p > ≡ x
+p-iso :  { x  : HOD } → (p : def ZFProduct (&  x) ) → < π1 p , π2 p > ≡ x
 p-iso {x} p = ord≡→≡ (op-iso p) 
 
-p-pi1 :  { x y : HOD } → (p : def ZFProduct (od→ord  < x , y >) ) →  π1 p ≡ x
+p-pi1 :  { x y : HOD } → (p : def ZFProduct (&  < x , y >) ) →  π1 p ≡ x
 p-pi1 {x} {y} p = proj1 ( prod-eq ( ord→== (op-iso p) ))
 
-p-pi2 :  { x y : HOD } → (p : def ZFProduct (od→ord  < x , y >) ) →  π2 p ≡ y
+p-pi2 :  { x y : HOD } → (p : def ZFProduct (&  < x , y >) ) →  π2 p ≡ y
 p-pi2 {x} {y} p = proj2 ( prod-eq ( ord→== (op-iso p)))
 
-ω-pair :  {x y : HOD} → {m : Ordinal} → od→ord x o< next m → od→ord y o< next m → od→ord (x , y) o< next m
+ω-pair :  {x y : HOD} → {m : Ordinal} → & x o< next m → & y o< next m → & (x , y) o< next m
 ω-pair lx ly = next< (omax<nx lx ly ) ho<
 
-ω-opair : {x y : HOD} → {m : Ordinal} → od→ord x o< next m → od→ord y o< next m → od→ord < x , y > o< next m
+ω-opair : {x y : HOD} → {m : Ordinal} → & x o< next m → & y o< next m → & < x , y > o< next m
 ω-opair {x} {y} {m} lx ly = lemma0 where
-    lemma0 : od→ord < x , y > o< next m
+    lemma0 : & < x , y > o< next m
     lemma0 = osucprev (begin
-         osuc (od→ord < x , y >)
+         osuc (& < x , y >)
        <⟨ osuc<nx ho< ⟩
-         next (omax (od→ord (x , x)) (od→ord (x , y)))
+         next (omax (& (x , x)) (& (x , y)))
        ≡⟨ cong (λ k → next k) (sym ( omax≤ _ _ pair-xx<xy )) ⟩
-         next (osuc (od→ord (x , y)))
+         next (osuc (& (x , y)))
        ≡⟨ sym (nexto≡) ⟩
-         next (od→ord (x , y))
+         next (& (x , y))
        ≤⟨ x<ny→≤next (ω-pair lx ly) ⟩
          next m
        ∎ ) where
@@ -159,23 +159,23 @@
 A ⊗ B  = Union ( Replace B (λ b → Replace A (λ a → < a , b > ) ))
 
 product→ : {A B a b : HOD} → A ∋ a → B ∋ b  → ( A ⊗ B ) ∋ < a , b >
-product→ {A} {B} {a} {b} A∋a B∋b = λ t → t (od→ord (Replace A (λ a → < a , b >)))
-             record { proj1 = lemma1 ; proj2 = subst (λ k → odef k (od→ord < a , b >)) (sym oiso) lemma2 } where
-    lemma1 :  odef (Replace B (λ b₁ → Replace A (λ a₁ → < a₁ , b₁ >))) (od→ord (Replace A (λ a₁ → < a₁ , b >)))
+product→ {A} {B} {a} {b} A∋a B∋b = λ t → t (& (Replace A (λ a → < a , b >)))
+             ⟪ lemma1 , subst (λ k → odef k (& < a , b >)) (sym *iso) lemma2 ⟫ where
+    lemma1 :  odef (Replace B (λ b₁ → Replace A (λ a₁ → < a₁ , b₁ >))) (& (Replace A (λ a₁ → < a₁ , b >)))
     lemma1 = replacement← B b B∋b
-    lemma2 : odef (Replace A (λ a₁ → < a₁ , b >)) (od→ord < a , b >)
+    lemma2 : odef (Replace A (λ a₁ → < a₁ , b >)) (& < a , b >)
     lemma2 = replacement← A a A∋a
 
-x<nextA : {A x : HOD} → A ∋ x →  od→ord x o< next (odmax A)
+x<nextA : {A x : HOD} → A ∋ x →  & x o< next (odmax A)
 x<nextA {A} {x} A∋x = ordtrans (c<→o< {x} {A} A∋x) ho<
 
-A<Bnext : {A B x : HOD} → od→ord A o< od→ord B → A ∋ x → od→ord x o< next (odmax B)
+A<Bnext : {A B x : HOD} → & A o< & B → A ∋ x → & x o< next (odmax B)
 A<Bnext {A} {B} {x} lt A∋x = osucprev (begin
-          osuc (od→ord x)  
+          osuc (& x)  
        <⟨ osucc (c<→o< A∋x) ⟩
-          osuc (od→ord A)
+          osuc (& A)
        <⟨ osucc lt ⟩
-          osuc (od→ord B)
+          osuc (& B)
        <⟨ osuc<nx ho<  ⟩
           next (odmax B)
        ∎ ) where open o≤-Reasoning O
@@ -186,21 +186,21 @@
    where
        lemma : (y : Ordinal) → ( ord-pair y ∧ ((p : ord-pair y) → odef A (pi1 p) ∧ odef B (pi2 p))) → y o< omax (next (odmax A)) (next (odmax B))
        lemma y lt with proj1 lt
-       lemma p lt | pair x y with trio< (od→ord A) (od→ord B) 
-       lemma p lt | pair x y | tri< a ¬b ¬c = ordtrans (ω-opair (A<Bnext a (subst (λ k → odef A k ) (sym diso)
+       lemma p lt | pair x y with trio< (& A) (& B) 
+       lemma p lt | pair x y | tri< a ¬b ¬c = ordtrans (ω-opair (A<Bnext a (subst (λ k → odef A k ) (sym &iso)
            (proj1 (proj2 lt (pair x y))))) (lemma1 (proj2 (proj2 lt (pair x y))))) (omax-y _ _ ) where
-               lemma1 : odef B y → od→ord (ord→od y) o< next (HOD.odmax B)
+               lemma1 : odef B y → & (* y) o< next (HOD.odmax B)
                lemma1 lt = x<nextA {B} (d→∋ B lt)
        lemma p lt | pair x y | tri≈ ¬a b ¬c = ordtrans (ω-opair (x<nextA {A} (d→∋ A ((proj1 (proj2 lt (pair x y)))))) lemma2 ) (omax-x _ _ ) where
-                lemma2 :  od→ord (ord→od y) o< next (HOD.odmax A)
-                lemma2 = ordtrans ( subst (λ k → od→ord (ord→od y) o< k ) (sym b) (c<→o< (d→∋ B ((proj2 (proj2 lt (pair x y))))))) ho<
+                lemma2 :  & (* y) o< next (HOD.odmax A)
+                lemma2 = ordtrans ( subst (λ k → & (* y) o< k ) (sym b) (c<→o< (d→∋ B ((proj2 (proj2 lt (pair x y))))))) ho<
        lemma p lt | pair x y | tri> ¬a ¬b c = ordtrans (ω-opair  (x<nextA {A} (d→∋ A ((proj1 (proj2 lt (pair x y))))))
-           (A<Bnext c (subst (λ k → odef B k ) (sym diso) (proj2 (proj2 lt (pair x y)))))) (omax-x _ _ ) 
+           (A<Bnext c (subst (λ k → odef B k ) (sym &iso) (proj2 (proj2 lt (pair x y)))))) (omax-x _ _ ) 
 
 ZFP⊆⊗ :  {A B : HOD} {x : Ordinal} → odef (ZFP A B) x → odef (A ⊗ B) x
-ZFP⊆⊗ {A} {B} {px} record { proj1 = (pair x y) ; proj2 = p2 } = product→ (d→∋ A (proj1 (p2 (pair x y) ))) (d→∋ B (proj2 (p2 (pair x y) )))
+ZFP⊆⊗ {A} {B} {px} ⟪ (pair x y) ,  p2 ⟫ = product→ (d→∋ A (proj1 (p2 (pair x y) ))) (d→∋ B (proj2 (p2 (pair x y) )))
 
 -- axiom of choice required
--- ⊗⊆ZFP : {A B x : HOD} → ( A ⊗ B ) ∋ x → def ZFProduct (od→ord x)
--- ⊗⊆ZFP {A} {B} {x} lt = subst (λ k → ord-pair (od→ord k )) {!!} op-cons
+-- ⊗⊆ZFP : {A B x : HOD} → ( A ⊗ B ) ∋ x → def ZFProduct (& x)
+-- ⊗⊆ZFP {A} {B} {x} lt = subst (λ k → ord-pair (& k )) {!!} op-cons
 
diff -r cb067605fea0 -r 44a484f17f26 VL.agda
--- a/VL.agda	Fri Jul 31 17:54:52 2020 +0900
+++ b/VL.agda	Sat Aug 01 11:06:29 2020 +0900
@@ -30,15 +30,21 @@
 --    V α := ⋃ { V β | β < α }
 
 V : ( β : Ordinal ) → HOD
-V β = TransFinite1  Vβ₁ β where
-   Vβ₁ : (x : Ordinal ) → ( ( y : Ordinal) → y o< x → HOD )  → HOD
-   Vβ₁ x Vβ₀ with trio< x o∅
-   Vβ₁ x Vβ₀ | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a)
-   Vβ₁ x Vβ₀ | tri≈ ¬a refl ¬c = Ord o∅
-   Vβ₁ x Vβ₀ | tri> ¬a ¬b c with Oprev-p  x
-   Vβ₁ x Vβ₀ | tri> ¬a ¬b c | yes p = Power ( Vβ₀ (Oprev.oprev p ) (subst (λ k → _ o< k) (Oprev.oprev=x  p) <-osuc ))
-   Vβ₁ x Vβ₀ | tri> ¬a ¬b c | no ¬p = 
-        record { od = record { def = λ y → (y o< x ) ∧ ((lt : y o< x ) →  odef (Vβ₀ y lt) x ) } ; odmax = x; <odmax = λ {x} lt → proj1 lt }
+V β = TransFinite1  V1 β where
+   V1 : (x : Ordinal ) → ( ( y : Ordinal) → y o< x → HOD )  → HOD
+   V1 x V0 with trio< x o∅
+   V1 x V0 | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a)
+   V1 x V0 | tri≈ ¬a refl ¬c = Ord o∅
+   V1 x V0 | tri> ¬a ¬b c with Oprev-p  x
+   V1 x V0 | tri> ¬a ¬b c | yes p = Power ( V0 (Oprev.oprev p ) (subst (λ k → _ o< k) (Oprev.oprev=x  p) <-osuc ))
+   V1 x V0 | tri> ¬a ¬b c | no ¬p = 
+        record { od = record { def = λ y → (y o< x ) ∧ ((lt : y o< x ) →  odef (V0 y lt) x ) } ; odmax = x; <odmax = λ {x} lt → proj1 lt }
+
+--
+-- L ⊆ HOD ⊆ V
+--
+-- HOD=V : (x : HOD) → V (odmax x) ∋ x
+-- HOD=V x = {!!}
 
 --
 -- Definition for Power Set
@@ -58,15 +64,15 @@
 --    V α := ⋃ { L β | β < α }
 
 L : ( β : Ordinal ) → Definitions → HOD
-L β D = TransFinite1  Lβ₁ β where
-   Lβ₁ : (x : Ordinal ) → ( ( y : Ordinal) → y o< x → HOD )  → HOD
-   Lβ₁ x Lβ₀ with trio< x o∅
-   Lβ₁ x Lβ₀ | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a)
-   Lβ₁ x Lβ₀ | tri≈ ¬a refl ¬c = Ord o∅
-   Lβ₁ x Lβ₀ | tri> ¬a ¬b c with Oprev-p  x
-   Lβ₁ x Lβ₀ | tri> ¬a ¬b c | yes p = Df D ( Lβ₀ (Oprev.oprev p ) (subst (λ k → _ o< k) (Oprev.oprev=x  p) <-osuc ))
-   Lβ₁ x Lβ₀ | tri> ¬a ¬b c | no ¬p = 
-        record { od = record { def = λ y → (y o< x ) ∧ ((lt : y o< x ) →  odef (Lβ₀ y lt) x ) } ; odmax = x; <odmax = λ {x} lt → proj1 lt }
+L β D = TransFinite1  L1 β where
+   L1 : (x : Ordinal ) → ( ( y : Ordinal) → y o< x → HOD )  → HOD
+   L1 x L0 with trio< x o∅
+   L1 x L0 | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a)
+   L1 x L0 | tri≈ ¬a refl ¬c = Ord o∅
+   L1 x L0 | tri> ¬a ¬b c with Oprev-p  x
+   L1 x L0 | tri> ¬a ¬b c | yes p = Df D ( L0 (Oprev.oprev p ) (subst (λ k → _ o< k) (Oprev.oprev=x  p) <-osuc ))
+   L1 x L0 | tri> ¬a ¬b c | no ¬p = 
+        record { od = record { def = λ y → (y o< x ) ∧ ((lt : y o< x ) →  odef (L0 y lt) x ) } ; odmax = x; <odmax = λ {x} lt → proj1 lt }
 
 V=L0 : Set (suc n)
 V=L0 = (x : Ordinal) → V x ≡  L x record { Definition = λ y → y }
diff -r cb067605fea0 -r 44a484f17f26 cardinal.agda
--- a/cardinal.agda	Fri Jul 31 17:54:52 2020 +0900
+++ b/cardinal.agda	Sat Aug 01 11:06:29 2020 +0900
@@ -33,7 +33,7 @@
 
 Func :  OD
 Func = record { def = λ x → def ZFProduct x
-    ∧ ( (a b c : Ordinal) → odef (ord→od x) (od→ord < ord→od a , ord→od b >) ∧ odef (ord→od x) (od→ord < ord→od a , ord→od c >) →  b ≡  c ) }  
+    ∧ ( (a b c : Ordinal) → odef (* x) (& < * a , * b >) ∧ odef (* x) (& < * a , * c >) →  b ≡  c ) }  
 
 FuncP :  ( A B : HOD ) → HOD
 FuncP A B = record { od = record { def = λ x → odef (ZFP A B) x
@@ -41,32 +41,32 @@
        ; odmax = odmax (ZFP A B) ; <odmax = λ lt → <odmax (ZFP A B) (proj1 lt) }
 
 Func∋f : {A B x : HOD} → ( f : HOD → HOD ) → ( (x : HOD ) → A ∋ x → B ∋ f x )
-    → def Func (od→ord  (Replace A (λ x → < x , f x > )))
+    → def Func (&  (Replace A (λ x → < x , f x > )))
 Func∋f = {!!}
 
 FuncP∋f : {A B x : HOD} → ( f : HOD → HOD ) → ( (x : HOD ) → A ∋ x → B ∋ f x )
-    → odef (FuncP A B) (od→ord  (Replace A (λ x → < x , f x > )))
+    → odef (FuncP A B) (&  (Replace A (λ x → < x , f x > )))
 FuncP∋f = {!!}
 
--- Func→f : {A B f x : HOD} → def Func (od→ord f)  → (x : HOD ) → A ∋ x  → ( HOD ∧ ((y : HOD ) → B ∋ y ))
+-- Func→f : {A B f x : HOD} → def Func (& f)  → (x : HOD ) → A ∋ x  → ( HOD ∧ ((y : HOD ) → B ∋ y ))
 -- Func→f = {!!}
--- Func₁ : {A B f : HOD} → def Func (od→ord f) → {!!}  
+-- Func₁ : {A B f : HOD} → def Func (& f) → {!!}  
 -- Func₁ = {!!}
--- Cod : {A B f : HOD} → def Func (od→ord f) → {!!}
+-- Cod : {A B f : HOD} → def Func (& f) → {!!}
 -- Cod = {!!}
--- 1-1 : {A B f : HOD} → def Func (od→ord f) → {!!}
+-- 1-1 : {A B f : HOD} → def Func (& f) → {!!}
 -- 1-1 = {!!}
--- onto : {A B f : HOD} → def Func (od→ord f) → {!!}
+-- onto : {A B f : HOD} → def Func (& f) → {!!}
 -- onto  = {!!}
 
 record Bijection (A B : Ordinal ) : Set n where
    field
        fun→ : Ordinal → Ordinal
        fun← : Ordinal → Ordinal
-       fun→inA : (x : Ordinal) → odef (ord→od A) ( fun→ x )
-       fun←inB : (x : Ordinal) → odef (ord→od B) ( fun← x )
-       fiso→ : (x : Ordinal ) → odef (ord→od B)  x → fun→ ( fun← x ) ≡ x
-       fiso← : (x : Ordinal ) → odef (ord→od A)  x → fun← ( fun→ x ) ≡ x
+       fun→inA : (x : Ordinal) → odef (* A) ( fun→ x )
+       fun←inB : (x : Ordinal) → odef (* B) ( fun← x )
+       fiso→ : (x : Ordinal ) → odef (* B)  x → fun→ ( fun← x ) ≡ x
+       fiso← : (x : Ordinal ) → odef (* A)  x → fun← ( fun→ x ) ≡ x
        
 Card : OD
 Card = record { def = λ x → (a : Ordinal) → a o< x → ¬ Bijection a x }
diff -r cb067605fea0 -r 44a484f17f26 filter.agda
--- a/filter.agda	Fri Jul 31 17:54:52 2020 +0900
+++ b/filter.agda	Sat Aug 01 11:06:29 2020 +0900
@@ -77,8 +77,8 @@
   ... | case1 p∈P  = case1 p∈P
   ... | case2 ¬p∈P = case2 (filter1 P {q ∩ (L ＼ p)} (∪-lemma2 (∈-filter P lt)) lemma7 lemma8) where
     lemma5 : ((p ∪ q ) ∩ (L ＼ p)) =h=  (q ∩ (L ＼ p))
-    lemma5 = record { eq→ = λ {x} lt → record { proj1 = lemma4 x lt ; proj2 = proj2 lt  }
-       ;  eq← = λ {x} lt → record { proj1 = case2 (proj1 lt) ; proj2 = proj2 lt }
+    lemma5 = record { eq→ = λ {x} lt → ⟪ lemma4 x lt , proj2 lt  ⟫
+       ;  eq← = λ {x} lt → ⟪  case2 (proj1 lt) , proj2 lt ⟫
       } where
          lemma4 : (x : Ordinal ) → odef ((p ∪ q) ∩ (L ＼ p)) x → odef q x
          lemma4 x lt with proj1 lt
@@ -105,8 +105,8 @@
         p+1-p=1 : {p : HOD} → p ⊆ L → L =h= (p ∪ (L ＼ p)) 
         eq→ (p+1-p=1 {p} p⊆L) {x} lt with ODC.decp O (odef p x)
         eq→ (p+1-p=1 {p} p⊆L) {x} lt | yes p∋x = case1 p∋x
-        eq→ (p+1-p=1 {p} p⊆L) {x} lt | no ¬p = case2 (record { proj1 = lt ; proj2 = ¬p })
-        eq← (p+1-p=1 {p} p⊆L) {x} ( case1 p∋x ) = subst (λ k → odef L k ) diso (incl p⊆L ( subst (λ k → odef p k) (sym diso) p∋x  )) 
+        eq→ (p+1-p=1 {p} p⊆L) {x} lt | no ¬p = case2 ⟪ lt , ¬p ⟫
+        eq← (p+1-p=1 {p} p⊆L) {x} ( case1 p∋x ) = subst (λ k → odef L k ) &iso (incl p⊆L ( subst (λ k → odef p k) (sym &iso) p∋x  )) 
         eq← (p+1-p=1 {p} p⊆L) {x} ( case2 ¬p  ) = proj1 ¬p
         lemma : (p : HOD) → p ⊆ L   →  filter P ∋ (p ∪ (L ＼ p))
         lemma p p⊆L = subst (λ k → filter P ∋ k ) (==→o≡ (p+1-p=1 p⊆L)) f∋L
diff -r cb067605fea0 -r 44a484f17f26 generic-filter.agda
--- a/generic-filter.agda	Fri Jul 31 17:54:52 2020 +0900
+++ b/generic-filter.agda	Sat Aug 01 11:06:29 2020 +0900
@@ -69,9 +69,9 @@
 data Hω2 :  (i : Nat) ( x : Ordinal  ) → Set n where
   hφ :  Hω2 0 o∅
   h0 : {i : Nat} {x : Ordinal  } → Hω2 i x  →
-    Hω2 (Suc i) (od→ord (Union ((< nat→ω i , nat→ω 0 >) ,  ord→od x )))
+    Hω2 (Suc i) (& (Union ((< nat→ω i , nat→ω 0 >) ,  * x )))
   h1 : {i : Nat} {x : Ordinal  } → Hω2 i x  →
-    Hω2 (Suc i) (od→ord (Union ((< nat→ω i , nat→ω 1 >) ,  ord→od x )))
+    Hω2 (Suc i) (& (Union ((< nat→ω i , nat→ω 1 >) ,  * x )))
   he : {i : Nat} {x : Ordinal  } → Hω2 i x  →
     Hω2 (Suc i) x
 
@@ -85,13 +85,13 @@
 HODω2 :  HOD
 HODω2 = record { od = record { def = λ x → Hω2r x } ; odmax = next o∅ ; <odmax = odmax0 } where
     P  : (i j : Nat) (x : Ordinal ) → HOD
-    P  i j x = ((nat→ω i , nat→ω i) , (nat→ω i , nat→ω j)) , ord→od x
-    nat1 : (i : Nat) (x : Ordinal) → od→ord (nat→ω i) o< next x
+    P  i j x = ((nat→ω i , nat→ω i) , (nat→ω i , nat→ω j)) , * x
+    nat1 : (i : Nat) (x : Ordinal) → & (nat→ω i) o< next x
     nat1 i x =  next< nexto∅ ( <odmax infinite (ω∋nat→ω {i}))
-    lemma1 : (i j : Nat) (x : Ordinal ) → osuc (od→ord (P i j x)) o< next x
+    lemma1 : (i j : Nat) (x : Ordinal ) → osuc (& (P i j x)) o< next x
     lemma1 i j x = osuc<nx (pair-<xy (pair-<xy (pair-<xy (nat1 i x) (nat1 i x) ) (pair-<xy (nat1 i x) (nat1 j x) ) )
-         (subst (λ k → k o< next x) (sym diso) x<nx ))
-    lemma : (i j : Nat) (x : Ordinal ) → od→ord (Union (P i j x)) o< next x
+         (subst (λ k → k o< next x) (sym &iso) x<nx ))
+    lemma : (i j : Nat) (x : Ordinal ) → & (Union (P i j x)) o< next x
     lemma i j x = next< (lemma1 i j x ) ho<
     odmax0 :  {y : Ordinal} → Hω2r y → y o< next o∅ 
     odmax0 {y} r with hω2 r
@@ -125,7 +125,7 @@
 ω→2f x lt n | no ¬p = i0
 
 fω→2-sel : ( f : Nat → Two ) (x : HOD) → Set n
-fω→2-sel f x = (infinite ∋ x) ∧ ( (lt : odef infinite (od→ord  x) ) → f (ω→nat x lt) ≡ i1 )
+fω→2-sel f x = (infinite ∋ x) ∧ ( (lt : odef infinite (&  x) ) → f (ω→nat x lt) ≡ i1 )
 
 fω→2 : (Nat → Two) → HOD
 fω→2 f = Select infinite (fω→2-sel f)
@@ -177,7 +177,7 @@
 --
 PGHOD :  (i : Nat) → (C : CountableOrdinal) → (P : HOD) → (p : Ordinal) → HOD
 PGHOD i C P p = record { od = record { def = λ x  →
-       odef P x ∧ odef (ord→od (ctl→ C i)) x  ∧  ( (y : Ordinal ) → odef (ord→od p) y →  odef (ord→od x) y ) }
+       odef P x ∧ odef (* (ctl→ C i)) x  ∧  ( (y : Ordinal ) → odef (* p) y →  odef (* x) y ) }
    ; odmax = odmax P  ; <odmax = λ {y} lt → <odmax P (proj1 lt) }  
 
 ---
@@ -186,7 +186,7 @@
 next-p :  (C : CountableOrdinal) (P : HOD ) (i : Nat) → (p : Ordinal) → Ordinal
 next-p C P i p with ODC.decp O ( PGHOD i C P p =h= od∅ )
 next-p C P i p | yes y = p
-next-p C P i p | no not = od→ord (ODC.minimal O (PGHOD i C P p ) not)
+next-p C P i p | no not = & (ODC.minimal O (PGHOD i C P p ) not)
 
 ---
 --  ascendant search on p(n)
@@ -201,7 +201,7 @@
 record PDN  (C : CountableOrdinal) (P : HOD ) (x : Ordinal) : Set n where
    field
        gr : Nat
-       pn<gr : (y : Ordinal) → odef (ord→od x) y → odef (ord→od (find-p C P gr o∅)) y
+       pn<gr : (y : Ordinal) → odef (* x) y → odef (* (find-p C P gr o∅)) y
        px∈ω  : odef (Power P) x
 
 open PDN
@@ -219,7 +219,7 @@
 --  Generic Filter on Power P for HOD's Countable Ordinal (G ⊆ Power P ≡ G i.e. Nat → P → Set )
 --
 --  p 0 ≡ ∅
---  p (suc n) = if ∃ q ∈ ord→od ( ctl→ n ) ∧ p n ⊆ q → q  (axiom of choice)
+--  p (suc n) = if ∃ q ∈ * ( ctl→ n ) ∧ p n ⊆ q → q  (axiom of choice)
 ---             else p n
 
 P-GenericFilter : (C : CountableOrdinal) → (P : HOD ) → GenericFilter P
@@ -229,17 +229,17 @@
    } where
         P∅ : {P : HOD} → odef (Power P) o∅
         P∅ {P} =  subst (λ k → odef (Power P) k ) ord-od∅ (lemma o∅  o∅≡od∅) where
-            lemma : (x : Ordinal ) → ord→od x ≡ od∅ → odef (Power P) (od→ord od∅)
+            lemma : (x : Ordinal ) → * x ≡ od∅ → odef (Power P) (& od∅)
             lemma x eq = power← P od∅  (λ {x} lt → ⊥-elim (¬x<0 lt ))
-        x<y→∋ : {x y : Ordinal} → odef (ord→od x) y → ord→od x ∋ ord→od y
-        x<y→∋ {x} {y} lt = subst (λ k → odef (ord→od x) k ) (sym diso) lt
-        find-p-⊆P : (C : CountableOrdinal) (P : HOD ) (i : Nat) → (x y : Ordinal)  → odef (Power P) x → odef (ord→od (find-p C P i x)) y → odef P y 
-        find-p-⊆P C P Zero x y Px Py = subst (λ k → odef P k ) diso
-            ( incl (ODC.power→⊆ O P (ord→od x) (d→∋ (Power P)  Px)) (x<y→∋ Py))
+        x<y→∋ : {x y : Ordinal} → odef (* x) y → * x ∋ * y
+        x<y→∋ {x} {y} lt = subst (λ k → odef (* x) k ) (sym &iso) lt
+        find-p-⊆P : (C : CountableOrdinal) (P : HOD ) (i : Nat) → (x y : Ordinal)  → odef (Power P) x → odef (* (find-p C P i x)) y → odef P y 
+        find-p-⊆P C P Zero x y Px Py = subst (λ k → odef P k ) &iso
+            ( incl (ODC.power→⊆ O P (* x) (d→∋ (Power P)  Px)) (x<y→∋ Py))
         find-p-⊆P C P (Suc i) x y Px Py = find-p-⊆P C P i (next-p C P i x)  y {!!} {!!}
         f⊆PL :  PDHOD C P ⊆ Power P
         f⊆PL = record { incl = λ {x} lt → power← P x (λ {y} y<x →
-             find-p-⊆P C P (gr lt) o∅ (od→ord y) P∅ (pn<gr lt (od→ord y) (subst (λ k → odef k (od→ord y)) (sym oiso) y<x))) }
+             find-p-⊆P C P (gr lt) o∅ (& y) P∅ (pn<gr lt (& y) (subst (λ k → odef k (& y)) (sym *iso) y<x))) }
 
 
 open GenericFilter
diff -r cb067605fea0 -r 44a484f17f26 logic.agda
--- a/logic.agda	Fri Jul 31 17:54:52 2020 +0900
+++ b/logic.agda	Sat Aug 01 11:06:29 2020 +0900
@@ -17,6 +17,7 @@
    false : Bool
 
 record  _∧_  {n m : Level} (A  : Set n) ( B : Set m ) : Set (n ⊔ m) where
+   constructor ⟪_,_⟫
    field
       proj1 : A
       proj2 : B
diff -r cb067605fea0 -r 44a484f17f26 ordinal.agda
--- a/ordinal.agda	Fri Jul 31 17:54:52 2020 +0900
+++ b/ordinal.agda	Sat Aug 01 11:06:29 2020 +0900
@@ -171,14 +171,14 @@
   →  ∀ (x : Ordinal)  → ψ x
 TransFinite {n} {m} {ψ} caseΦ caseOSuc x = proj1 (TransFinite1 (lv x) (ord x) ) where
   TransFinite1 : (lx : Nat) (ox : OrdinalD lx ) → ψ (ordinal lx ox) ∧ ( ( (x : Ordinal {suc n} ) → x o< ordinal lx ox  → ψ x ) )
-  TransFinite1 Zero (Φ 0) = record { proj1 = caseΦ Zero lemma ; proj2 = lemma1 } where
+  TransFinite1 Zero (Φ 0) = ⟪  caseΦ Zero lemma , lemma1 ⟫ where
       lemma : (x : Ordinal) → x o< ordinal Zero (Φ Zero) → ψ x
       lemma x (case1 ())
       lemma x (case2 ())
       lemma1 : (x : Ordinal) → x o< ordinal Zero (Φ Zero) → ψ x
       lemma1 x (case1 ())
       lemma1 x (case2 ())
-  TransFinite1 (Suc lx) (Φ (Suc lx)) = record { proj1 = caseΦ (Suc lx) (λ x → lemma (lv x) (ord x)) ; proj2 = (λ x → lemma (lv x) (ord x)) } where
+  TransFinite1 (Suc lx) (Φ (Suc lx)) = ⟪ caseΦ (Suc lx) (λ x → lemma (lv x) (ord x)) , (λ x → lemma (lv x) (ord x)) ⟫ where
       lemma0 : (ly : Nat) (oy : OrdinalD ly ) → ordinal ly oy  o< ordinal lx (Φ lx) → ψ (ordinal ly oy)
       lemma0 ly oy lt = proj2 ( TransFinite1 lx (Φ lx) ) (ordinal ly oy) lt
       lemma : (ly : Nat) (oy : OrdinalD ly ) → ordinal ly oy  o< ordinal (Suc lx) (Φ (Suc lx)) → ψ (ordinal ly oy)
@@ -197,7 +197,7 @@
           lemma2 y lt2 | case2 (case1 lt3) = proj2 (TransFinite1 lx (Φ lx)) y (case1 (<-trans lt3 lt1 ))
           lemma2 y lt2 | case2 (case2 lt3) with d<→lv lt3
           ... | refl = proj2 (TransFinite1 lx (Φ lx)) y (case1 lt1)
-  TransFinite1 lx (OSuc lx ox)  = record { proj1 = caseOSuc lx ox lemma ; proj2 = lemma } where
+  TransFinite1 lx (OSuc lx ox)  = ⟪ caseOSuc lx ox lemma , lemma ⟫ where
       lemma : (y : Ordinal) → y o< ordinal lx (OSuc lx ox) → ψ y
       lemma y lt with osuc-≡< lt
       lemma y lt | case1 refl = proj1 ( TransFinite1 lx ox )