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

diff -r ebc18df12f5a -r b7c2a67befdf src/HyperReal.agda
--- a/src/HyperReal.agda	Fri Jul 02 22:58:09 2021 +0900
+++ b/src/HyperReal.agda	Sat Jul 03 10:46:55 2021 +0900
@@ -32,33 +32,12 @@
 
 open _∧_
 
-     -- t1 :  nxn→n 0 1 ≡ 1
-     -- t1 = refl
-     -- t2 :  nxn→n 1 0 ≡ 2
-     -- t2 = refl
-     -- t3 :  nxn→n 0 2 ≡ 3
-     -- t3 = refl
-     -- t4 :  nxn→n 1 1 ≡ 4
-     -- t4 = refl
-     -- t5 :  nxn→n 2 0 ≡ 5
-     -- t5 = refl
-     -- t6 :  nxn→n 0 3 ≡ 6
-     -- t6 = refl
-     -- t7 :  nxn→n 1 2 ≡ 7
-     -- t7 = refl
-     -- t8 :  nxn→n 2 1 ≡ 8
-     -- t8 = refl
-     -- t9 :  nxn→n 3 0 ≡ 9
-     -- t9 = refl
-     -- t10 :  nxn→n 0 4 ≡ 10
-     -- t10 = refl
-
 nxn : NxN
 nxn = record {
      nxn→n = λ p → nxn→n (proj1 p) (proj2 p)
    ; n→nxn =  n→nxn 
-   ; nn-id = {!!}
-   ; n-id = {!!}
+   ; nn-id = nn-id
+   ; n-id = n-id
   } where
      nxn→n :  ℕ →  ℕ → ℕ
      nxn→n zero zero = zero
@@ -70,18 +49,31 @@
      n→nxn (suc i) with n→nxn i
      ... | ⟪ x , zero ⟫ = ⟪ zero  , suc x ⟫
      ... | ⟪ x , suc y ⟫ = ⟪ suc x , y ⟫
+     nid1 : (i : ℕ) → 0 < proj2 ( n→nxn i)  → n→nxn (suc i) ≡ ⟪ suc (proj1 ( n→nxn i )) , pred ( proj2 ( n→nxn i )) ⟫
+     nid1 (suc i) 0<p2 with  n→nxn (suc i) | inspect  n→nxn (suc i)
+     ... | ⟪ x , zero ⟫ | record { eq = eq } = {!!}
+     ... | ⟪ x , suc y ⟫ | record { eq = eq } = refl
+     nid2 : (i j : ℕ) → suc (nxn→n i (suc j)) ≡ nxn→n (suc i) j 
+     nid2 zero zero = refl
+     nid2 zero (suc j) = refl
+     nid2 (suc i) zero = {!!}
+     nid2 (suc i) (suc j) = {!!}
+     n-id :  (i : ℕ) → nxn→n (proj1 (n→nxn i)) (proj2 (n→nxn i)) ≡ i
+     n-id 0 = refl
+     n-id (suc i) with proj2 (n→nxn (suc i)) 
+     ... | zero = {!!}
+     ... | suc x = begin
+          nxn→n (proj1 (n→nxn (suc i))) (suc x)   ≡⟨ {!!} ⟩
+          nxn→n (proj1 (n→nxn i)) (suc x)   ≡⟨ {!!} ⟩
+          nxn→n (proj1 (n→nxn i)) (proj2 (n→nxn i))   ≡⟨ {!!} ⟩
+          i   ≡⟨ {!!} ⟩
+          suc i ∎ where open ≡-Reasoning
+     f : (i : ℕ) → Set
+     f i = n→nxn (suc i) ≡ ⟪ suc (proj1 ( n→nxn i )) , pred ( proj2 ( n→nxn i )) ⟫
+     g : (i j : ℕ) → Set
+     g i j = suc (nxn→n i (suc j)) ≡ nxn→n (suc i) j 
      nn-id : (i j : ℕ) → n→nxn (nxn→n i j) ≡ ⟪ i , j ⟫
-     nn-id zero zero = refl
-     nn-id zero (suc j) with  n→nxn (j + (nxn→n 0 j))
-     ... | ⟪ x , zero ⟫ = {!!}
-     ... | ⟪ x , suc y ⟫ = {!!}
-     --= begin
-     --   n→nxn (nxn→n zero (suc j)) ≡⟨ refl ⟩ --  n→nxn (nxn→n zero j) ≡ ⟪ zero , j ⟫ : nn-id zero j
-     --   n→nxn (j + suc (nxn→n 0 j))  ≡⟨  {!!}  ⟩
-     --   n→nxn (suc (j + (nxn→n 0 j)))  ≡⟨  {!!}  ⟩
-     --   {!!}  ≡⟨  {!!}  ⟩
-     --   ⟪ zero , suc j ⟫ ∎  where open ≡-Reasoning
-     nn-id (suc i) j = {!!}
+     nn-id = {!!}
 
 open NxN