最近はarXivで3本ほど気になる論文が出ている。

1. N. Najmaei, N. van der Weide, B. Ahrens, and P. R. North, “A Type Theory for Comprehension Categories with Applications to Subtyping”.
2. B. Ahrens, A. Lafont, and T. Lamiaux, “2-Functoriality of Initial Semantics, and Applications”.
3. S. Krishnan and E. Rudman, “A convenient category of cubes”.

3本目は軽く流し読みした。Cubeの圏って実は色々な変種が出ていて、それらを良い感じに抽象化する圏を定義しているようだ。特にcubeの間の射の定義が簡潔になっているらしい。Cubical setまわりはまだあまり把握できていないので今すぐ読み込む必要のある論文ではなかったが、cubeの圏がcubical type theory以外にも様々の応用がなされていることを知れたのはよかった。まあ単体的集合の圏の内部言語とcubical setの圏の内部言語が似た振る舞いをするのであれば、topologyやhomotopy theory勢がcubeの圏に関心を持つのは不思議なことではないのかもしれない。

1本目はタイトルだけだとあまり面白く見えないかもしれないが、comprehension category周りの研究の流れを知っていると中々興味深い進展となっている、はず。Category with familiesは閉じた型を集合の元として解釈するのに対し、comprehension categoryは圏の対象として解釈する。ここの差分が部分型付けと関係することは以前から言われていて(2023年のCategorical models of subtyping)、おそらく著者も被っているだろう、と思ったら被っていなかった。この論文は時間をかけて読みたい。ところでNajmaei以外の3人の名前は見たことがあるが、Najmaeiは初めて見た。Lafontの元で博士課程の学生をやっているらしい。