新しい Agda

Sets (集合を対象、写像を射とする圏)の Completeness としばらく格闘していたんですが... Compleness ってのは Limit があることで、Limit ってのは、与えられた関手で示された対象と射のグラフ上の可換関係を代表する対象みたいなものらしい。

直積とかは二つの要素の代表なんだけど、それがあれば、その二つの要素にできることは全部できるじゃないですか。そんな感じ。

なんだが、なかなかできなくて。結局、

  record snat   { c₂ }  { I OC :  Set  c₂ } ( sobj :  OC →  Set  c₂ )
       ( smap : { i j :  OC  }  → (f : I ) →  sobj i → sobj j ) : Set  c₂ where
     field
         snmap : ( i : OC ) → sobj i
          sncommute : ( i j : OC ) → ( f :  I ) →  smap f ( snmap i )  ≡ snmap j
     smap0 :  { i j :  OC  }  → (f : I ) →  sobj i → sobj j
     smap0 {i} {j} f x =  smap f x

という record を作れば Limit の uniquness 以外は簡単に示せました。なのだが、uniquness が堅い。要するに、field 二つが等しければ、record 自体が等しいという合同性の問題らしい。

でも、ググってたら、にたようなのを Stack Over Flow で見つけました。(良くある)

https://stackoverflow.com/questions/37488098/equality-on-dependent-record-types

なのだが、こいつの例題が通らない。もしかして、Agda の version の問題か? 確かにちょっと古いんだよな。

で、update をかけたんですが... なんか、emacs も update。あ、てめーちょっと待て。

emacs 25 に上げられてしまったおかげで、xterm 上の色とかUTF8がずれまくる。vim は大丈夫なんだけど。くそ、unusable だ。しかも。Agda は 25 でないと動かない。

GUIでしか動かさないあほが手を入れて xterm 側を壊してるんだよな。

で、肝心の例題は Agda のupdate で通ったんですが、Sets completeness の方は通らず。くそ〜 どうも問題は Agda のrecord の合同性の扱いそのものにあるっぽい。僕のせいじゃないらしいです。

    snat-cong :  { c : Level }  { I OC :  Set  c }  { SObj :  OC →  Set  c  } { SMap : { i j :  OC  }  → (f : I )→  SObj i → SObj j }
                 ( s t :  snat SObj SMap   )
             → ( ( λ i  → snmap s i )  ≡  ( λ i →  snmap t i ) )
             → ( ( λ i j f →  smap0 s f ( snmap s i )  ≡ snmap s j   ) ≡  (  ( λ  i j f → smap0 t f ( snmap t i )  ≡ snmap t j ) ) )
             → s ≡ t
    snat-cong s t refl refl = refl

が通るはず。だけど、通らない。これはあきらめた方が良さそう。

なので、Agda 壊れちゃったので、ちょっと困ってます。vim で編集して emacs でチェックみたいな感じ。