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

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

• https://m-hiyama.hatenablog.com/entry/2020/10/21/175259

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

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

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