--- a/src/HyperReal.agda	Fri Jul 02 07:42:52 2021 +0900
+++ b/src/HyperReal.agda	Fri Jul 02 12:39:52 2021 +0900
@@ -13,21 +13,91 @@
 HyperNat : Set
 HyperNat = ℕ → ℕ
 
+record NxN : Set where
+  field
+     nxn→n : ℕ ∧ ℕ → ℕ
+     n→nxn : ℕ → ℕ ∧ ℕ 
+     nn-id : (i j : ℕ) →  n→nxn (nxn→n ⟪ i , j ⟫ ) ≡ ⟪ i , j ⟫
+     n-id : (i  : ℕ) →  nxn→n (n→nxn i ) ≡ i
+
+open _∧_
+
+     -- t1 :  nxn→n 0 1 ≡ 1
+     -- t1 = refl
+     -- t2 :  nxn→n 1 0 ≡ 2
+     -- t2 = refl
+     -- t3 :  nxn→n 0 2 ≡ 3
+     -- t3 = refl
+     -- t4 :  nxn→n 1 1 ≡ 4
+     -- t4 = refl
+     -- t5 :  nxn→n 2 0 ≡ 5
+     -- t5 = refl
+     -- t6 :  nxn→n 0 3 ≡ 6
+     -- t6 = refl
+     -- t7 :  nxn→n 1 2 ≡ 7
+     -- t7 = refl
+     -- t8 :  nxn→n 2 1 ≡ 8
+     -- t8 = refl
+     -- t9 :  nxn→n 3 0 ≡ 9
+     -- t9 = refl
+     -- t10 :  nxn→n 0 4 ≡ 10
+     -- t10 = refl
+
+nxn : NxN
+nxn = record {
+     nxn→n = λ p → nxn→n (proj1 p) (proj2 p)
+   ; n→nxn =  n→nxn 
+   ; nn-id = {!!}
+   ; n-id = {!!}
+  } where
+     nxn→n :  ℕ →  ℕ → ℕ
+     nxn→n zero zero = zero
+     nxn→n zero (suc j) = j + suc (nxn→n zero j)
+     nxn→n (suc i) zero = suc i + suc (nxn→n i zero)
+     nxn→n (suc i) (suc j) = suc i + suc j + suc (nxn→n i (suc j))
+     n→nxn : ℕ → ℕ ∧ ℕ
+     n→nxn zero = ⟪ 0 , 0 ⟫
+     n→nxn (suc i) with n→nxn i
+     ... | ⟪ x , zero ⟫ = ⟪ zero  , suc x ⟫
+     ... | ⟪ x , suc y ⟫ = ⟪ suc x , y ⟫
+     nn-id : (i j : ℕ) → n→nxn (nxn→n i j) ≡ ⟪ i , j ⟫
+     nn-id zero zero = refl
+     nn-id zero (suc j) with  n→nxn (j + (nxn→n 0 j))
+     ... | ⟪ x , zero ⟫ = {!!}
+     ... | ⟪ x , suc y ⟫ = {!!}
+     --= begin
+     --   n→nxn (nxn→n zero (suc j)) ≡⟨ refl ⟩ --  n→nxn (nxn→n zero j) ≡ ⟪ zero , j ⟫ : nn-id zero j
+     --   n→nxn (j + suc (nxn→n 0 j))  ≡⟨  {!!}  ⟩
+     --   n→nxn (suc (j + (nxn→n 0 j)))  ≡⟨  {!!}  ⟩
+     --   {!!}  ≡⟨  {!!}  ⟩
+     --   ⟪ zero , suc j ⟫ ∎  where open ≡-Reasoning
+     nn-id (suc i) j = {!!}
+
+open NxN
+
+n1 : ℕ → ℕ
+n1 n = proj1 (n→nxn nxn n)
+
+n2 : ℕ → ℕ
+n2 n = proj2 (n→nxn nxn n)
+
 _n*_ : (i j : HyperNat ) → HyperNat
 
 _n+_ : (i j : HyperNat ) → HyperNat
-i n+ j = λ k → i k + j k
-
-i n* j = λ k → i k * j k
+i n+ j = λ k → i (n1 k) + j (n2 k)
 
--- _n<_ : ?
-
--- postulate
---    _cmpHN_  : ( i j HyperNat ) → Dec ( i n< j )
+i n* j = λ k → i (n1 k) * j (n2 k)
 
 hzero : HyperNat
 hzero _ = 0 
 
+_n≤_ : (i j : HyperNat ) → Set -- ?
+i n≤ j = (k : ℕ ) → i k ≤ j k
+
+postulate
+   _cmpn_  : ( i j : HyperNat ) → Dec ( i n≤ j )
+
+
 data HyperZ : Set where
    hz : HyperNat → HyperNat → HyperZ 
 
@@ -42,21 +112,36 @@
 HNzero : HyperNat → Set
 HNzero i = ( k : ℕ ) →  i k ≡ 0 
 
+≤→= : {i j : ℕ} → i ≤ j → j ≤ i → i ≡ j
+≤→= {0} {0} z≤n z≤n = refl
+≤→= {suc i} {suc j} (s≤s i<j) (s≤s j<i) = cong suc ( ≤→= {i} {j} i<j j<i )
+
 HNzero? : ( i : HyperNat ) → Dec (HNzero i)
-HNzero? i = {!!} where
-   HNz1  : ( m k : ℕ ) → k < m → Dec (( j : ℕ ) → ( j < k ) → i j ≡ 0 )
-   HNz1 (suc m) zero k<m with i 0 ≟ 0
-   ... | yes y  = yes {!!}
-   ... | no n  = no (λ n1 → {!!} )
-   HNz1 (suc m) (suc k) (s≤s k<m) with HNz1 m k k<m
-   ... | yes y = yes {!!}
-   ... | no n = no ( λ n1 → {!!} )
+HNzero? i with i cmpn hzero | hzero cmpn i
+... | no s | t = no (λ n → s (λ k → subst (λ k → k ≤ 0) (sym (n k)) refl-≤ )) --  (k₁ : ℕ) → i k₁ ≡ 0  → i k ≤ 0
+... | s | no t = no (λ n → t (λ k → subst (λ k → 0 ≤ k) (sym (n k)) refl-≤ ))
+... | yes s | yes t = yes (λ k → ≤→= (s k) (t k))
+
+record HNzeroK ( x : HyperNat ) : Set where
+  field
+     nonzero : ℕ
+     isNonzero : ¬ ( x nonzero ≡ 0 )
+
+postulate 
+   HNnzerok : (x  : HyperNat ) → ¬ ( HNzero x ) → HNzeroK x
+
+import Axiom.Extensionality.Propositional
+postulate f-extensionality : { n m : Level}  → Axiom.Extensionality.Propositional.Extensionality n m
+
+m*n=0⇒m=0∨n=0 : {i j : ℕ} → i * j ≡ 0 → (i ≡ 0) ∨ ( j ≡ 0 )
+m*n=0⇒m=0∨n=0 {zero} {j} refl = case1 refl
+m*n=0⇒m=0∨n=0 {suc i} {zero} eq = case2 refl
 
 HNnzero* : {x y : HyperNat } → ¬ ( HNzero x ) → ¬ ( HNzero y ) → ¬ ( HNzero (x n* y) )
-HNnzero* {x} {y} nzx nzy nzx*y with HNzero? x | HNzero? y
-... | yes t | s = ⊥-elim ( nzx t )
-... | t | yes s = ⊥-elim ( nzy s )
-... | no t | no s = {!!}
+HNnzero* {x} {y} nzx nzy nzx*y with HNnzerok x nzx | HNnzerok y nzy
+... | s | t = {!!} where
+   hnz0 : ( k : ℕ ) → x k * y k ≡ 0  → (x k ≡ 0) ∨ (y k ≡ 0)
+   hnz0 k x*y = m*n=0⇒m=0∨n=0 x*y 
 
 
 HZzero : HyperZ → Set