日々の流転

λ. “The Path Category in ALF and AGDA” by Ilya Beylin

We compare different definitions of the path category in type theory and two of its implementations, ALF and AGDA. For our purposes, both ALF and AGDA implement the logical framework of [NPS90], but support two different versions of inductive definitions. It appears that in ALF we can define the path category in a natural way, and in AGDA it is not possible.

を読んだ。

圏を型理論で形式化するときには、以下の二つの流儀がある。

1. Obj, Arr ∈ Set と src, target ∈ Arr → Obj で扱う方法
2. Obj ∈ Set と Hom ∈ Obj → Obj → Set で扱う方法

が、後者の流儀でHomをSetoidにした E-category が、色々な概念を自然に形式化することが出来て良いそうだ。

それで、Path category (有向グラフから自由生成される圏で、元のグラフの頂点が対象、元のグラフのパスが射になる) を Alf と Agda で書くとどうなるかという話。 当時の Agda には inductive families がなかったのでパスのデータ型が定義できなかった。

λ. お菓子買いだめ

買いだめというほどではなくなってしまったけど。