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 either as a map , so that and is (or contains) the collection of the , or as a map , so that and is the disjoint union of the (where is the index of the set to which 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" . 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.

（ ´_ゝ｀）フーン