--- a/src/HyperReal.agda	Thu Mar 18 16:55:49 2021 +0900
+++ b/src/HyperReal.agda	Fri Jul 02 07:42:52 2021 +0900
@@ -7,39 +7,79 @@
 open import Level renaming ( suc to succ ; zero to Zero )
 open import  Relation.Binary.PropositionalEquality hiding ( [_] )
 open import Relation.Binary.Definitions
+open import nat
+open import logic
 
-hnzero : (ℕ → ℕ) → Set
-hnzero f = (x : ℕ) → ¬ ( x ≡ zero )
+HyperNat : Set
+HyperNat = ℕ → ℕ
+
+_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
+
+-- _n<_ : ?
 
-data HyperReal : Set where
-   hnat :  (ℕ → ℕ) → HyperReal
-   hadd :  HyperReal → (x : ℕ → ℕ ) → HyperReal
-   hsub :  HyperReal → (x : ℕ → ℕ ) → HyperReal
-   hdiv :  HyperReal → (x : ℕ → ℕ ) → hnzero x → HyperReal
+-- postulate
+--    _cmpHN_  : ( i j HyperNat ) → Dec ( i n< j )
+
+hzero : HyperNat
+hzero _ = 0 
+
+data HyperZ : Set where
+   hz : HyperNat → HyperNat → HyperZ 
 
-data Rational : Set where
-   rat :  ℕ → ℕ → (z : ℕ) → ¬ (z ≡ zero)  → Rational  -- (x - y ) / z
+_z*_ : (i j : HyperZ ) → HyperZ
+
+_z+_ : (i j : HyperZ ) → HyperZ
+hz i i₁ z+ hz j j₁ = hz ( i n+ j ) (i₁ n+ j₁ )
 
-prat : Rational → ℕ
-prat (rat x _ _ _ ) = x
+--   ( i - i₁ ) * ( j - j₁ ) = i * j + i₁ * j₁ - i * j₁ - i₁ * j
+hz i i₁ z* hz j j₁ = hz (λ k → i k * j k + i₁ k * j₁ k ) (λ k →  i k * j₁ k - i₁ k * j k )
+
+HNzero : HyperNat → Set
+HNzero i = ( k : ℕ ) →  i k ≡ 0 
 
-mrat : Rational → ℕ
-mrat (rat _ y _ _ ) = y
+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 → {!!} )
 
-drat : Rational → ℕ
-drat (rat _ _ z _ ) = z
+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 = {!!}
 
-zrat : (r : Rational ) → ¬ (drat r ≡ zero) 
-zrat (rat _ _ z ne ) = ne
+
+HZzero : HyperZ → Set
+HZzero (hz i j ) = ( k : ℕ ) →  i k ≡ j k 
 
-HyRa←R : HyperReal → (ℕ → Rational)
-HyRa←R (hnat x) i = rat (x i) 0 1 (λ ())
-HyRa←R (hadd x y) i with HyRa←R x i
-... | rat w v z ne = rat (w + z * (y i)) v z ne
-HyRa←R (hsub x y) i  with HyRa←R x i
-... | rat w v z ne = rat w (v + z * (y i)) z ne
-HyRa←R (hdiv x y nz) i with HyRa←R x i
-... | rat w v z ne = rat w v (z * (y i)) {!!}
+HZzero? : ( i : HyperZ ) → Dec (HZzero i)
+HZzero? = {!!}
+
+data HyperR : Set where
+   hr :  HyperZ → (k : HyperNat ) → ¬ HNzero k → HyperR
 
-HyR←Ra :  (ℕ → Rational) → HyperReal
-HyR←Ra r = hdiv (hsub (hnat (λ i → prat (r i))) (λ i → mrat (r i))) (λ i → drat (r i)) {!!}
+HZnzero* : {x y : HyperZ } → ¬ ( HZzero x ) → ¬ ( HZzero y ) → ¬ ( HZzero (x z* y) )
+HZnzero* {x} {y} nzx nzy nzx*y with HZzero? x | HZzero? y
+... | yes t | s = ⊥-elim ( nzx t )
+... | t | yes s = ⊥-elim ( nzy s )
+... | no t | no s = {!!}
+
+HRzero : HyperR → Set
+HRzero (hr i j nz ) = HZzero i
+
+_h*_ : (i j : HyperR) → HyperR
+
+_h+_ : (i j : HyperR) → HyperR
+hr x k nz h+ hr y k₁ nz₁ = hr ( (x z* (hz k hzero)) z+  (y z* (hz k₁ hzero)) ) (k n* k₁) (HNnzero* nz nz₁)
+
+hr x k nz h* hr y k₁ nz₁ = hr ( x z* y ) ( k n* k₁ ) (HNnzero* nz nz₁)