bonotakeの日記

元・ソフトウェア工学系研究者、今・AI系エンジニア

indexed category と fibred category

最近 indexed category と fibred category が頭の中でごっちゃになっていたところ、以前の日記のコメントでタナカさんが紹介してくれたレビューに面白い一説を発見した。以下引用。

There are two fairly obvious ways one could treat "indexing": thinking of sets and functions for the moment, we can regard an indexed family of sets  \{X_i | i \in I \} either as a map  X: I \to {\bf X}, so that X(i) = X_i and {\bf X} is (or contains) the collection of the X_i, or as a map  X: {\bf X} \to I, so that X^{-1}(i) = X_i and {\bf X} is the disjoint union of the X_i (where X(x) is the index of the set to which x belongs). The first approach leads to the notion of "indexed category", and has the advantage that initially it seems more intuitive and technically simpler; its main conceptual drawback is that it places the emphasis on the individual "fibres" X_i. The second approach, which emphasizes the global entity that represents the family of sets, leads to the notion of fibration. It has the advantage that it avoids the axiom of choice in places where it really is unnecessary, and so permits the description of canonical constructions; essentially, this means that the principal notions of importance are properties of a structure, rather than being additional structure. Also fibrations make the modular approach mentioned above much more straightforward.
(snip)
The ability to compose fibrations makes this approach to semantics technically more flexible and more powerful; it is the essence of this algebraic approach to type theory and proof theory, and compared to it, other approaches often seem contrived.

( ´_ゝ`)フーン

注:bonotakeは、amazon.co.jpを宣伝しリンクすることによってサイトが紹介料を獲得できる手段を提供することを目的に設定されたアフィリエイト宣伝プログラムである、 Amazonアソシエイト・プログラムの参加者です。