--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/.gitignore	Thu Mar 18 16:55:49 2021 +0900
@@ -0,0 +1,8 @@
+### Agda ###
+*.agdai
+*.hi
+*.o
+*.agda#
+*.agda~
+.#*.agda
+./agda-stdlib
\ No newline at end of file

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/HyperReal.agda-lib	Thu Mar 18 16:55:49 2021 +0900
@@ -0,0 +1,5 @@
+-- File generated by Agda-Pkg
+name:    HyperReal
+depend:  standard-library
+include: src
+-- End 

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/HyperReal.agda-pkg	Thu Mar 18 16:55:49 2021 +0900
@@ -0,0 +1,16 @@
+# File generated by Agda-Pkg
+name:              HyperReal
+version:           v0.0.1
+
+
+homepage:          https://ie.u-ryukyu.ac.jp/~kono
+license:           MIT
+license-file:      LICENSE.md
+
+tested-with:       2.6.1.2
+description:       HyperReal is an Agda library ...
+depend:
+    - standard-library
+include:
+    - src
+# End 

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HyperReal.agda	Thu Mar 18 16:55:49 2021 +0900
@@ -0,0 +1,45 @@
+module HyperReal where
+
+open import Data.Nat
+open import Data.Nat.Properties
+open import Data.Empty
+open import Relation.Nullary using (¬_; Dec; yes; no)
+open import Level renaming ( suc to succ ; zero to Zero )
+open import  Relation.Binary.PropositionalEquality hiding ( [_] )
+open import Relation.Binary.Definitions
+
+hnzero : (ℕ → ℕ) → Set
+hnzero f = (x : ℕ) → ¬ ( x ≡ zero )
+
+data HyperReal : Set where
+   hnat :  (ℕ → ℕ) → HyperReal
+   hadd :  HyperReal → (x : ℕ → ℕ ) → HyperReal
+   hsub :  HyperReal → (x : ℕ → ℕ ) → HyperReal
+   hdiv :  HyperReal → (x : ℕ → ℕ ) → hnzero x → HyperReal
+
+data Rational : Set where
+   rat :  ℕ → ℕ → (z : ℕ) → ¬ (z ≡ zero)  → Rational  -- (x - y ) / z
+
+prat : Rational → ℕ
+prat (rat x _ _ _ ) = x
+
+mrat : Rational → ℕ
+mrat (rat _ y _ _ ) = y
+
+drat : Rational → ℕ
+drat (rat _ _ z _ ) = z
+
+zrat : (r : Rational ) → ¬ (drat r ≡ zero) 
+zrat (rat _ _ z ne ) = ne
+
+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)) {!!}
+
+HyR←Ra :  (ℕ → Rational) → HyperReal
+HyR←Ra r = hdiv (hsub (hnat (λ i → prat (r i))) (λ i → mrat (r i))) (λ i → drat (r i)) {!!}