超準解析を Agda で

うっかり書き始めてしまったわけですが、わりと順調。

超自然数は

　　HyperNat = ℕ → ℕ

整数は差を取れば良い。

　　data HyperZ : Set where
　　　 hz : HyperNat → HyperNat → HyperZ

で分数と。

　　data HyperR : Set where
　　　 hr :　HyperZ → (k : HyperNat ) → ((i : ℕ) → 0 < k i) → HyperR

等号とか不等号の決定はTrichotomous は排中律な仮定になるわけですけどね。

　　record _n≤_　(i j : HyperNat ) :　Set where
　　　 field
　　　　　≤-map : Bijection ℕ ℕ
　　　　　≤-m : ℕ
　　　　　is-n≤ : (k : ℕ ) → k > ≤-m → i k ≤ j (fun→ ≤-map　k)

ってな感じか。これで、できそうなんですが、

Transfer principle ってのがあって「実数で証明できる性質は、超実数でも証明される」ってのがあるらしい。

確かに、自然数から上の方法で分数まで作って体になるので、そうなるんだが、それ自体をどう Agda で書くのかわからん。

　　transferN : ( p : ℕ → Set ) → HyperNat → Set
　　transferN p n = (k : ℕ ) → p (n k)

　　transfer : {R H : Set} → ( p : R ∨ H → Set )
　　　　 → ((x : R ) →　p (case1 x) )
　　　　 → ((x : H ) →　p (case2 x))
　　transfer {R} {h} p rp x = ?

ってなのを思いついたが、それで通るのかは謎だな。