--- a/src/HyperReal.agda	Thu Jul 08 08:40:51 2021 +0900
+++ b/src/HyperReal.agda	Thu Jul 08 11:55:40 2021 +0900
@@ -52,11 +52,19 @@
 
 open _n≤_
 
-_n<_ :  (i j : HyperNat ) → Set
-i n< j = ( i n+ h 1 ) n≤ j 
+record _n<_  (i j : HyperNat ) :  Set where 
+   field 
+      <-map : Bijection ℕ ℕ
+      <-m : ℕ
+      is-<≤ : (k : ℕ ) → k > <-m → i k < j (fun→ <-map  k)
+
+open _n<_
+
+_n<=s≤_ :  (i j : HyperNat ) → (i n< j) ⇔ (( i n+ h 1 ) n≤ j )
+_n<=s≤_ = {!!}
 
 postulate
-   _cmpn_  : ( i j : HyperNat ) → Dec ( i n< j )
+   _cmpn_  : Trichotomous {Level.zero} _n=_  _n<_ 
 
 n=IsEquivalence : IsEquivalence _n=_
 n=IsEquivalence = record { refl = record {=-map = bid ℕ ; =-m = 0 ; is-n= = λ _ _ → refl}
@@ -68,14 +76,25 @@
      isPreorder = record {
               isEquivalence = n=IsEquivalence
             ; reflexive     = λ eq → record { ≤-map = =-map eq ; ≤-m = =-m eq ; is-n≤ = {!!} }
-            ; trans         = {!!} }
-    ; total = {!!}
-  }
+            ; trans         = trans1 }
+    ; total = total
+  } where
+      open import Data.Sum.Base using (_⊎_)
+      open _⊎_
+      total : (x y : HyperNat ) → (x n≤ y) ⊎ (y n≤ x)
+      total x y with x cmpn y
+      ... | tri< a ¬b ¬c = inj₁ {!!}
+      ... | tri≈ ¬a b ¬c = {!!}
+      ... | tri> ¬a ¬b c = {!!}
+      trans1 : {i j k : HyperNat} →  i n≤ j → j n≤ k → i n≤ k
+      trans1 = {!!}
 
 
 data HyperZ : Set where
    hz : HyperNat → HyperNat → HyperZ 
 
+hZ : ℕ → ℕ → HyperZ
+hZ x y = hz (λ _ → x) (λ _ → y )
 
 _z+_ : (i j : HyperZ ) → HyperZ
 hz i i₁ z+ hz j j₁ = hz ( i n+ j ) (i₁ n+ j₁ )
@@ -83,36 +102,26 @@
 _z*_ : (i j : HyperZ ) → HyperZ
 hz i i₁ z* hz j j₁ = hz (λ k → i k * j k + i₁ k * j₁ k ) (λ k →  i k * j₁ k - i₁ k * j k )
 
-HNzero : HyperNat → Set
-HNzero i = ( k : ℕ ) →  i k ≡ 0 
-
+--  x0 - y0 ≡ x1 - y1
+--  x0 + y1 ≡ x1 + y0
+--
 _z=_ :  (i j : HyperZ ) → Set
-_z=_ = {!!}
+_z=_ (hz x0 y0) (hz x1 y1)  = (x0 n+ y1) n= (x1 n+ y0)
 
 _z≤_ :  (i j : HyperZ ) → Set
-_z≤_ = {!!}
-
+_z≤_ (hz x0 y0) (hz x1 y1)  = (x0 n+ y1) n≤ (x1 n+ y0)
 
-HNzero? : ( i : HyperNat ) → Dec (HNzero i)
-HNzero? i with i cmpn hzero | hzero cmpn i
-... | no s | t = no (λ n → s {!!}) --  (k₁ : ℕ) → i k₁ ≡ 0  → i k ≤ 0
-... | s | no t = no (λ n → t {!!})
-... | yes s | yes t = yes (λ k → {!!} )
+_z<_ :  (i j : HyperZ ) → Set
+_z<_ (hz x0 y0) (hz x1 y1)  = (x0 n+ y1) n< (x1 n+ y0)
 
-record HNzeroK ( x : HyperNat ) : Set where
-  field
-     nonzero : ℕ
-     isNonzero : ¬ ( x nonzero ≡ 0 )
-
-postulate 
-   HNnzerok : (x  : HyperNat ) → ¬ ( HNzero x ) → HNzeroK x
+_cmpz_  : Trichotomous {Level.zero}  _z=_ _z<_
+(hz x0 y0)  cmpz (hz x1 y1)  = (x0 n+ y1) cmpn (x1 n+ y0) 
 
 import Axiom.Extensionality.Propositional
 postulate f-extensionality : { n m : Level}  → Axiom.Extensionality.Propositional.Extensionality n m
 
-HNnzero* : {x y : HyperNat } → ¬ ( HNzero x ) → ¬ ( HNzero y ) → ¬ ( HNzero (x n* y) )
-HNnzero* {x} {y} nzx nzy nzx*y with HNnzerok x nzx | HNnzerok y nzy
-... | s | t = {!!} where
+HNnzero* : {x y : HyperNat } → ¬ ( x n= h 0 ) → ¬ ( y n= h 0  ) → ¬ ( (x n* y) n= h 0 )
+HNnzero* {x} {y} nzx nzy nzx*y = {!!} where
    hnz0 : ( k : ℕ ) → x k * y k ≡ 0  → (x k ≡ 0) ∨ (y k ≡ 0)
    hnz0 k x*y = m*n=0⇒m=0∨n=0 x*y 
 
@@ -124,7 +133,7 @@
 HZzero? = {!!}
 
 data HyperR : Set where
-   hr :  HyperZ → (k : HyperNat ) → ¬ HNzero k → HyperR
+   hr :  HyperZ → (k : HyperNat ) → ¬ (k n= h 0) → HyperR
 
 HZnzero* : {x y : HyperZ } → ¬ ( HZzero x ) → ¬ ( HZzero y ) → ¬ ( HZzero (x z* y) )
 HZnzero* {x} {y} nzx nzy nzx*y with HZzero? x | HZzero? y
@@ -135,6 +144,9 @@
 HRzero : HyperR → Set
 HRzero (hr i j nz ) = HZzero i
 
+hR :  ℕ → ℕ → (k : HyperNat ) → ¬ (k n= h 0) → HyperR
+hR x y k ne = hr (hZ x y) k ne
+
 _h=_ :  (i j : HyperR ) → Set
 _h=_ = {!!}
 
@@ -142,8 +154,20 @@
 _h≤_ = {!!}
 
 _h*_ : (i j : HyperR) → HyperR
+hr x k nz h* hr y k₁ nz₁ = hr ( x z* y ) ( k n* k₁ ) (HNnzero* nz nz₁)
 
 _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* y ) ( k n* k₁ ) (HNnzero* nz nz₁)
+HyperReal :  Set 
+HyperReal = ℕ  → HyperR
+
+HR→HRl : HyperR → HyperReal
+HR→HRl (hr (hz x y) k ne) k1 = hr (hz (λ k2 → (x k1)) (λ k2 → (x k1))) k ne
+
+HRl→HR : HyperReal → HyperR
+HRl→HR r = hr (hz (λ k → {!!}) (λ k → {!!}) ) factor {!!} where
+   factor : HyperNat 
+   factor n = {!!}
+   fne : (n : ℕ) → ¬ (factor n= h 0)
+   fne = ?