--- a/src/HyperReal.agda	Fri Jul 09 08:08:39 2021 +0900
+++ b/src/HyperReal.agda	Fri Jul 09 11:11:10 2021 +0900
@@ -188,6 +188,9 @@
 R0 : HyperR
 R0 = hr (hZ 0 0) (h 1) {!!}
 
+R1 : HyperR
+R1 = hr (hZ 1 0) (h 1) {!!}
+
 record Rational : Set where
   field
      rp rm k : ℕ
@@ -199,6 +202,9 @@
 rH : (r : Rational ) → HyperR
 rH r =  hr (hZ (Rational.rp r) (Rational.rm r)) (h (Rational.k r)) {!!}
 
+nH : (r : ℕ ) → HyperR
+nH r =  hr (hZ r 0) (h 1) {!!}
+
 --
 --  z0 / y0 = z1 / y1 ← z0 * y1 = z1 * y0
 --
@@ -256,7 +262,8 @@
       standard          : HyperR → HyperR
       is-standard       : {x : HyperR } → x ≈ standard x
       standard-unique   : {x y : HyperR } →  x ≈ y → standard x ≡ standard y
-      st-inifinitesimal : {x : HyperR } → inifinitesimal-R x → st x ≡ R0
+      st-inifinitesimal : {x : HyperR } → inifinitesimal-R x → standard x ≡ R0
+      st-ℕ : {x : HyperR } → { i : ℕ } → x ≈ nH i → standard x ≡ nH i
 
 postulate
    ST : Standard
@@ -266,5 +273,23 @@
 st :  HyperR → HyperR
 st x = standard ST x
 
+open import Algebra.Structures
+open import Algebra.Bundles
+
+HRing : CommutativeRing Level.zero Level.zero
+HRing = record {
+       Carrier           = HyperR
+    ;  _≈_               = _h=_
+    ;  _+_               = _h+_
+    ;  _*_               = _h*_
+    ;  -_                = -h
+    ;  0#                = R0
+    ;  1#                = R1
+    ;  isCommutativeRing = {!!}
+  }
 
 
+transfer : ( p : Rational ∨ HyperR → Set ) 
+     → ((x : Rational ) →  p (case1 x) )
+     → ((x : HyperR ) →  p (case2 x)) 
+transfer = {!!}