うっかり書き始めてしまったわけですが、わりと順調。
超自然数は
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 = ?
ってなのを思いついたが、それで通るのかは謎だな。
No comments:
Post a Comment