2006-05-14 [長年日記]
λ. A groupoid model refutes uniqueness of identity proofs. Martin Hofmann and Thomas Streicher.
- <URL:http://ieeexplore.ieee.org/xpls/abs_all.jsp?arnumber=316071>
- <URL:http://www.citeulike.org/article/602344>
を読んだ。groupoidの圏とfibrationを使って、Idの要素がequalityでなくgroupoidのendomorphismを表すようなモデルを作る話。そうすると、nontrivialなendomorphismが存在するgroupoidについてはIdは複数の要素を持つ。言っていることはそんなに難しくはないのだが、indexed-category とか presheaf とか fibration とか grothendieck construction とか 2 category とかに不慣れ*1なことと、一部にインフォーマルな表記がされていることから、きちんと追いかけるのが大変だった。大変だったけどその分これらに少しは馴染めたような気がするが……
まあ、なんにせよ、Propositional equality の証明の equalityでの悩みはとりあえず解決か。
*1 不慣れなこと多すぎ!
λ. NやList(N)のUIP
上記論文によると、NやList(N)のような型に関しては「UIP is actually syntactically derivable in the presense of a universe」らしいのだが、どうやるのかわからん。とりあえずゼロの場合は以下のように証明出来たのだが……
--#include "Hedberg/SET.alfa"
open SET use Id, refId, Unit, tt, Nat, zero, succ
Lem (x,y::Nat) (p::Id x y) :: Set
= case x of
(zer )-> case y of
(zer )-> Id p (refId zero)
(suc m)-> Unit
(suc m)-> Unit
lem (x,y::Nat) (p::Id x y) :: Lem x y p
= case p of
(ref z)-> case z of
(zer )-> refId (refId z)
(suc m)-> tt
prop (p::Id zero zero) :: Id p (refId zero)
prop = lem zero zero p
【2006-05-18 追記】 二日くらい必死で考えてようやく証明できたが……これ死ねるよ*1。termination-checkerは通らないけど、引数が小さくなっているのは明らかだからとりあえず良いよね。綺麗に書き直すのはまた今度ということで。それはそうと、Universeの強力さを初めて実感した。
--#include "Hedberg/SET.alfa"
open SET use Id, refId, substId, Nat, zero, succ, Zero
uipNat (n::Nat) (p::Id n n) :: Id (refId n) p
uipNat =
let T (|n1,|n2::Nat) (p::Id (succ n1) (succ n2)) (q::Id n1 n2) :: Set
= case q of
(ref x)-> Id (refId (succ x)) p
lemT (x,y::Nat) (p::Id x y) :: Set
= case x of
(zer )->
case y of
(zer )-> Id (refId zero) p
(suc y')-> Zero
(suc x')->
case y of
(zer )-> Zero
(suc y')-> (q::Id x' y') -> T p q
lem (x,y::Nat) (p::Id x y) :: lemT x y p
= case p of
(ref n)->
case n of
(zer )-> refId (refId zero)
(suc m)->
\(q::Id m m) ->
let lem2 :: Id (refId m) q
lem2 = uipNat m q
lem3 :: T p (refId m)
lem3 = refId (refId (succ m))
lem4 :: T p q
lem4 = substId (\q -> T p q) lem2 lem3
in lem4
in case n of
(zer )-> lem n n p
(suc m)-> lem n n p (refId m)
*1 試行錯誤の途中でAgdaのバグ(?)も踏んだしね
λ. 単相性制限 (monomorphism restriction)
<URL:http://d.hatena.ne.jp/a-san/20060511>の話。 普段は気にしないし、避けるのは難しくないのだけど、こういうときに説明に困ってしまうな。
メモ。
λ. ブルバキとモーニング娘。と
<URL:http://d.hatena.ne.jp/yaneurao/20060514> での「ブルバキみたいなやっちゃな」「そう、日本ではモーニング娘。ていうんだよ」というやり取りが少し面白かった。
