Journal of Formalized Mathematics
Volume 13, 2001
University of Bialystok
Copyright (c) 2001 Association of Mizar Users

Miscellaneous Facts about Functors


Grzegorz Bancerek
University of Bialystok, Shinshu University, Nagano

Summary.

In the paper we show useful facts concerning reverse and inclusion functors and the restriction of functors. We also introduce a new notation for the intersection of categories and the isomorphism under arbitrary functors.

MML Identifier: YELLOW20

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

Contents (PDF format)

  1. Reverse Functors
  2. Intersection of Categories
  3. Subcategories
  4. Inclusion Functors and Functor Restrictions
  5. Isomorphisms under Arbitrary Functor

Bibliography

[1] Grzegorz Bancerek. Concrete categories. Journal of Formalized Mathematics, 13, 2001.
[2] Czeslaw Bylinski. Basic functions and operations on functions. Journal of Formalized Mathematics, 1, 1989.
[3] Czeslaw Bylinski. Binary operations. Journal of Formalized Mathematics, 1, 1989.
[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. Partial functions. Journal of Formalized Mathematics, 1, 1989.
[7] Czeslaw Bylinski. Some basic properties of sets. Journal of Formalized Mathematics, 1, 1989.
[8] Czeslaw Bylinski. The modification of a function by a function and the iteration of the composition of a function. Journal of Formalized Mathematics, 2, 1990.
[9] Artur Kornilowicz. The composition of functors and transformations in alternative categories. Journal of Formalized Mathematics, 10, 1998.
[10] Malgorzata Korolkiewicz. Homomorphisms of many sorted algebras. Journal of Formalized Mathematics, 6, 1994.
[11] Beata Madras. Product of family of universal algebras. Journal of Formalized Mathematics, 5, 1993.
[12] Michal Muzalewski and Wojciech Skaba. Three-argument operations and four-argument operations. Journal of Formalized Mathematics, 2, 1990.
[13] Andrzej Trybulec. Tarski Grothendieck set theory. Journal of Formalized Mathematics, Axiomatics, 1989.
[14] Andrzej Trybulec. Tuples, projections and Cartesian products. Journal of Formalized Mathematics, 1, 1989.
[15] Andrzej Trybulec. Many-sorted sets. Journal of Formalized Mathematics, 5, 1993.
[16] Andrzej Trybulec. Many sorted algebras. Journal of Formalized Mathematics, 6, 1994.
[17] Andrzej Trybulec. Categories without uniqueness of \rm cod and \rm dom. Journal of Formalized Mathematics, 7, 1995.
[18] Andrzej Trybulec. Examples of category structures. Journal of Formalized Mathematics, 8, 1996.
[19] Andrzej Trybulec. Functors for alternative categories. Journal of Formalized Mathematics, 8, 1996.
[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.
[22] Edmund Woronowicz. Relations defined on sets. Journal of Formalized Mathematics, 1, 1989.

Received July 31, 2001

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