A Dependent Type Theory with Names and Binding http://www2.tcs.ifi.lmu.de/~schoepp/Docs/bunches.pdf を読んだ。 分離論理でも使うbunch演算子("*")を使って、含む名前が互いに素であることを表現するような依存型理論の話。
確かに、分離論理(separation logic)での、互い素なヒープ領域だけ言及するという性質は、互いに素な名前だけ言及するというのと全く同じで、言われてみれば当たり前なんだけれど、すごく面白かった。
そのうえで、フレッシュな名前によるweakeningを行う関手Wの左右の随伴 Σ* ⊣ W ⊣ Π* を考えると、Π* (magic wand "-*" の依存型版)は名前でパラメータ化したようなHOAS的な関数的な型に、Σ*はα-同値類的な型になる。
Schanuel topos はこの型理論の、Σ*_N ≅ Π*_N (と幾つかの追加条件) を満たすモデルになっていて、名前を含む値に対して、HOAS的な取扱いと、α-同値類的な取扱いの両方を、自由に使うことができる。
私は Fraenkel-Mostowski (FM) 集合論とか Schanuel topos とか知らなかったけれど、この辺りの話も面白そうかな。