# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1625796670 -32400
# Node ID 942f4e528a797d8bfc8a60f23efba0e138a87af1
# Parent  5e4b38745a396d1dcae06f91820e7a35b9300a47
...

diff -r 5e4b38745a39 -r 942f4e528a79 .gitignore
--- a/.gitignore	Fri Jul 09 08:08:39 2021 +0900
+++ b/.gitignore	Fri Jul 09 11:11:10 2021 +0900
@@ -5,4 +5,6 @@
 *.agda#
 *.agda~
 .#*.agda
-./agda-stdlib
\ No newline at end of file
+./agda-stdlib
+MAlonzo/**
+_build
diff -r 5e4b38745a39 -r 942f4e528a79 LICENSE.md
--- a/LICENSE.md	Fri Jul 09 08:08:39 2021 +0900
+++ b/LICENSE.md	Fri Jul 09 11:11:10 2021 +0900
@@ -0,0 +1,21 @@
+MIT License
+
+Copyright (c) 2021 Shinji KONO
+
+Permission is hereby granted, free of charge, to any person obtaining a copy
+of this software and associated documentation files (the "Software"), to deal
+in the Software without restriction, including without limitation the rights
+to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+copies of the Software, and to permit persons to whom the Software is
+furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in all
+copies or substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
+SOFTWARE.
diff -r 5e4b38745a39 -r 942f4e528a79 README.md
--- a/README.md	Fri Jul 09 08:08:39 2021 +0900
+++ b/README.md	Fri Jul 09 11:11:10 2021 +0900
@@ -0,0 +1,2 @@
+# HyperReal-in-agda
+HyperReal-in-agda
diff -r 5e4b38745a39 -r 942f4e528a79 src/HyperReal.agda
--- 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 = {!!}