依存型理論とファイバー付き圏

型カインドの定義は次にある。

これだと、単に「型の集合」だが、排他的型カインドという概念を入れないとまずいな。

排他的型カインドと型ファミリー(型でインデックスされた型の族)をしっかり区別して、シグマ型とパイ型の特性をきちんと定義する。

依存型理論とファイバー付き圏論の類似性から色々と分かる。