Journal of Formalized Mathematics
Volume 7, 1995
University of Bialystok
Copyright (c) 1995 Association of Mizar Users

Indexed Category


Grzegorz Bancerek
Institute of Mathematics, Polish Academy of Sciences

Summary.

The concept of indexing of a category (a part of indexed category, see [14]) is introduced as a pair formed by a many sorted category and a many sorted functor. The indexing of a category $C$ against to [14] is not a functor but it can be treated as a functor from $C$ into some categorial category (see [1]). The goal of the article is to work out the notation necessary to define institutions (see [11]).

MML Identifier: INDEX_1

The terminology and notation used in this paper have been introduced in the following articles [15] [8] [20] [16] [21] [4] [5] [7] [18] [17] [19] [12] [3] [6] [9] [10] [2] [13] [1]

Contents (PDF format)

  1. Category-yielding Functions
  2. Pairs of Many Sorted Sets
  3. Indexing
  4. Indexing vs Functors
  5. Composing Indexings and Functors

Bibliography

[1] Grzegorz Bancerek. Categorial categories and slice categories. Journal of Formalized Mathematics, 6, 1994.
[2] Grzegorz Bancerek and Agata Darmochwal. Comma category. Journal of Formalized Mathematics, 4, 1992.
[3] Grzegorz Bancerek and Piotr Rudnicki. On defining functions on trees. Journal of Formalized Mathematics, 5, 1993.
[4] Czeslaw Bylinski. Functions and their basic properties. Journal of Formalized Mathematics, 1, 1989.
[5] Czeslaw Bylinski. Functions from a set to a set. Journal of Formalized Mathematics, 1, 1989.
[6] Czeslaw Bylinski. Introduction to categories and functors. Journal of Formalized Mathematics, 1, 1989.
[7] Czeslaw Bylinski. Partial functions. Journal of Formalized Mathematics, 1, 1989.
[8] Czeslaw Bylinski. Some basic properties of sets. Journal of Formalized Mathematics, 1, 1989.
[9] Czeslaw Bylinski. Subcategories and products of categories. Journal of Formalized Mathematics, 2, 1990.
[10] Czeslaw Bylinski. Opposite categories and contravariant functors. Journal of Formalized Mathematics, 3, 1991.
[11] Joseph A. Goguen and Rod M. Burstall. Introducing institutions. \em Lecture Notes in Computer Science, 164:221--256, 1984.
[12] Beata Madras. Product of family of universal algebras. Journal of Formalized Mathematics, 5, 1993.
[13] Yatsuka Nakamura, Piotr Rudnicki, Andrzej Trybulec, and Pauline N. Kawamoto. Preliminaries to circuits, I. Journal of Formalized Mathematics, 6, 1994.
[14] Andrzej Tarlecki, Rod M. Burstall, and A. Goguen, Joseph. Some fundamental algebraic tools for the semantics of computation: Part 3. indexed categories. \em Theoretical Computer Science, 91:239--264, 1991.
[15] Andrzej Trybulec. Tarski Grothendieck set theory. Journal of Formalized Mathematics, Axiomatics, 1989.
[16] Andrzej Trybulec. Tuples, projections and Cartesian products. Journal of Formalized Mathematics, 1, 1989.
[17] Andrzej Trybulec. Function domains and Fr\aenkel operator. Journal of Formalized Mathematics, 2, 1990.
[18] Andrzej Trybulec. Many-sorted sets. Journal of Formalized Mathematics, 5, 1993.
[19] Andrzej Trybulec. Many sorted algebras. Journal of Formalized Mathematics, 6, 1994.
[20] Zinaida Trybulec. Properties of subsets. Journal of Formalized Mathematics, 1, 1989.
[21] Edmund Woronowicz. Relations and their basic properties. Journal of Formalized Mathematics, 1, 1989.

Received June 8, 1995


[ Download a postscript version, MML identifier index, Mizar home page]