--- a/src/HyperReal.agda	Thu Jul 08 14:23:36 2021 +0900
+++ b/src/HyperReal.agda	Thu Jul 08 17:14:30 2021 +0900
@@ -92,6 +92,22 @@
       trans1 : {i j k : HyperNat} →  i n≤ j → j n≤ k → i n≤ k
       trans1 = {!!}
 
+record n-finite (i : HyperNat ) : Set where
+  field
+     val : ℕ
+     is-val : i n= h val
+
+n-infinite :  (i : HyperNat ) → Set
+n-infinite i = (j : ℕ ) → h j n≤ i
+
+n-linear : HyperNat
+n-linear i = i
+
+n-linear-is-infnite : n-infinite n-linear
+n-linear-is-infnite i = record { ≤-map = bid ℕ ; ≤-m = i ; is-n≤ = λ k lt → <to≤ lt }
+
+¬-infinite-n-finite :  (i : HyperNat ) →  n-finite i → ¬ n-infinite i
+¬-infinite-n-finite = {!!}
 
 data HyperZ : Set where
    hz : HyperNat → HyperNat → HyperZ 
@@ -120,6 +136,18 @@
 <-cmpz  : Trichotomous {Level.zero}  _z=_ _z<_
 <-cmpz (hz x0 y0) (hz x1 y1)  = <-cmpn (x0 n+ y1) (x1 n+ y0) 
 
+-z :  (i : HyperZ ) →  HyperZ 
+-z (hz x y) = hz y x 
+
+z-z=0 : (i : HyperZ ) → (i z+ (-z i)) z= hZ 0 0
+z-z=0 = {!!}
+
+z+infinite :  (i : HyperZ ) → Set
+z+infinite i = (j : ℕ ) → hZ j 0 z≤ i
+
+z-infinite :  (i : HyperZ ) → Set
+z-infinite i = (j : ℕ ) → i z≤ hZ 0 j
+
 import Axiom.Extensionality.Propositional
 postulate f-extensionality : { n m : Level}  → Axiom.Extensionality.Propositional.Extensionality n m
 
@@ -149,7 +177,7 @@
 HZzero? = {!!}
 
 data HyperR : Set where
-   hr :  HyperZ → (k : HyperNat ) → ¬ (k n= h 0) → HyperR
+   hr :  HyperZ → (k : HyperNat ) → ((i : ℕ) → 0 < k i) → HyperR
 
 HZnzero* : {x y : HyperZ } → ¬ ( HZzero x ) → ¬ ( HZzero y ) → ¬ ( HZzero (x z* y) )
 HZnzero* {x} {y} nzx nzy nzx*y = {!!}
@@ -157,9 +185,20 @@
 HRzero : HyperR → Set
 HRzero (hr i j nz ) = HZzero i
 
-hR :  ℕ → ℕ → (k : HyperNat ) → ¬ (k n= h 0) → HyperR
+R0 : HyperR
+R0 = hr (hZ 0 0) (h 1) {!!}
+
+record Rational : Set where
+  field
+     rp rm k : ℕ
+     0<k : 0 < k
+
+hR :  ℕ → ℕ → (k : HyperNat ) → ((i : ℕ) → 0 < k i) → HyperR
 hR x y k ne = hr (hZ x y) k ne
 
+rH : (r : Rational ) → HyperR
+rH r =  hr (hZ (Rational.rp r) (Rational.rm r)) (h (Rational.k r)) {!!}
+
 --
 --  z0 / y0 = z1 / y1 ← z0 * y1 = z1 * y0
 --
@@ -176,10 +215,22 @@
 <-cmph (hr z0 k0 ne0 ) ( hr z1 k1 ne1 ) = <-cmpz  (z0 z* (hz k1 (h 0)))  (z1 z* (hz k0 (h 0)))
 
 _h*_ : (i j : HyperR) → HyperR
-hr x k nz h* hr y k₁ nz₁ = hr ( x z* y ) ( k n* k₁ ) (HNnzero* nz nz₁)
+hr x k nz h* hr y k₁ nz₁ = hr ( x z* y ) ( k n* k₁ ) {!!}
 
 _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* (hz k hzero)) z+  (y z* (hz k₁ hzero)) ) (k n* k₁) {!!}
+
+-h : (i : HyperR) → HyperR
+-h (hr x k nz) = hr (-z x) k nz
+
+inifinitesimal-R : (inf : HyperR) → Set
+inifinitesimal-R inf = ( r : Rational ) → R0 h< rH r → ( -h (rH r) h< inf ) ∧ ( inf h< rH r)
+
+1/x : HyperR
+1/x = hr (hZ 1 0) n-linear {!!}
+
+1/x-is-inifinitesimal : inifinitesimal-R 1/x
+1/x-is-inifinitesimal r 0<r = ⟪ {!!} , {!!} ⟫
 
 HyperReal :  Set 
 HyperReal = ℕ  → HyperR
@@ -193,3 +244,15 @@
    factor n = {!!}
    fne : (n : ℕ) → ¬ (factor n= h 0)
    fne = {!!}
+
+_≈_ : (x y : HyperR ) → Set
+x ≈ y = inifinitesimal-R (x h+ ( -h y )) 
+
+record Real : Set
+   field
+      st          : HyperR → HyperR
+      is-st       : (x : HyperR ) → x ≈ st x
+      st-unique   : (x y : HyperR ) → st x ≡ st y
+
+
+