# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1625234289 -32400
# Node ID ebc18df12f5a75aa85871770dbb0d60a462de436
# Parent  f094694aeec564dab280b626950e19db9217f8f8
...

diff -r f094694aeec5 -r ebc18df12f5a src/HyperReal.agda
--- a/src/HyperReal.agda	Fri Jul 02 22:00:15 2021 +0900
+++ b/src/HyperReal.agda	Fri Jul 02 22:58:09 2021 +0900
@@ -15,6 +15,14 @@
 HyperNat : Set
 HyperNat = ℕ → ℕ
 
+record IsoN : Set where
+  field
+     m→ m← : ℕ → ℕ 
+     id→← : (i  : ℕ) →  m→ (m← i ) ≡ i
+     id←→ : (i  : ℕ) →  m← (m→ i ) ≡ i
+
+open IsoN 
+
 record NxN : Set where
   field
      nxn→n : ℕ ∧ ℕ → ℕ
@@ -22,7 +30,6 @@
      nn-id : (i j : ℕ) →  n→nxn (nxn→n ⟪ i , j ⟫ ) ≡ ⟪ i , j ⟫
      n-id : (i  : ℕ) →  nxn→n (n→nxn i ) ≡ i
 
-
 open _∧_
 
      -- t1 :  nxn→n 0 1 ≡ 1
@@ -94,19 +101,31 @@
 hzero : HyperNat
 hzero _ = 0 
 
+record _n=_  (i j : HyperNat ) :  Set where 
+   field 
+      =-map : IsoN
+      =-m : ℕ
+      is-n= : (k : ℕ ) → k > =-m → i k ≡ j (m→ =-map  k)
+
 --
 --
 record _n≤_  (i j : HyperNat ) :  Set where 
    field 
-      ≤-map : ℕ → ℕ
+      ≤-map : IsoN
       ≤-m : ℕ
-      is-n≤ : (k : ℕ ) → k > ≤-m → i k ≤ j (≤-map k)
+      is-n≤ : (k : ℕ ) → k > ≤-m → i k ≤ j (m→ ≤-map  k)
 
 postulate
    _cmpn_  : ( i j : HyperNat ) → Dec ( i n≤ j )
 
-HNTotalOrder : IsTotalPreorder HyperNat ? _n≤_ 
-HNTotalOrder = ?
+HNTotalOrder : IsTotalPreorder _n=_ _n≤_ 
+HNTotalOrder = record {
+     isPreorder = record {
+              isEquivalence = {!!}
+            ; reflexive     = {!!}
+            ; trans         = {!!} }
+    ; total = {!!}
+  }
 
 
 data HyperZ : Set where
@@ -123,6 +142,12 @@
 HNzero : HyperNat → Set
 HNzero i = ( k : ℕ ) →  i k ≡ 0 
 
+_z=_ :  (i j : HyperZ ) → Set
+_z=_ = {!!}
+
+_z≤_ :  (i j : HyperZ ) → Set
+_z≤_ = {!!}
+
 ≤→= : {i j : ℕ} → i ≤ j → j ≤ i → i ≡ j
 ≤→= {0} {0} z≤n z≤n = refl
 ≤→= {suc i} {suc j} (s≤s i<j) (s≤s j<i) = cong suc ( ≤→= {i} {j} i<j j<i )
@@ -175,6 +200,12 @@
 HRzero : HyperR → Set
 HRzero (hr i j nz ) = HZzero i
 
+_h=_ :  (i j : HyperR ) → Set
+_h=_ = {!!}
+
+_h≤_ :  (i j : HyperR ) → Set
+_h≤_ = {!!}
+
 _h*_ : (i j : HyperR) → HyperR
 
 _h+_ : (i j : HyperR) → HyperR