Volume 7, 1995

University of Bialystok

Copyright (c) 1995 Association of Mizar Users

**Grzegorz Bancerek**- Institute of Mathematics, Polish Academy of Sciences

- 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]).

- Category-yielding Functions
- Pairs of Many Sorted Sets
- Indexing
- Indexing vs Functors
- Composing Indexings and Functors

- [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.

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