Volume 8, 1996

University of Bialystok

Copyright (c) 1996 Association of Mizar Users

**Claus Zinn**- University of Erlangen--N\"urnberg
**Wolfgang Jaksch**- University of Erlangen--N\"urnberg

- This article presents some theorems about functor structures. We start with some basic lemmata concerning the composition of functor structures. Then, two theorems about the restriction operator are formulated. Later we show two theorems concerning the properties 'full' and 'faithful' of functor structures which are equivalent to the 'onto' and 'one-to-one' properties of their morphmaps, respectively. Furthermore, we prove some theorems about the inversion of functor structures.

- Definitions
- Theorems about sets and functions
- Theorems about the composition of functor structures
- Theorems about the restriction and inclusion operator
- Theorems about 'full' and 'faithful' functor structures
- Theorems about the inversion of functor structures

- [1]
Czeslaw Bylinski.
Basic functions and operations on functions.
*Journal of Formalized Mathematics*, 1, 1989. - [2]
Czeslaw Bylinski.
Binary operations.
*Journal of Formalized Mathematics*, 1, 1989. - [3]
Czeslaw Bylinski.
Functions and their basic properties.
*Journal of Formalized Mathematics*, 1, 1989. - [4]
Czeslaw Bylinski.
Functions from a set to a set.
*Journal of Formalized Mathematics*, 1, 1989. - [5]
Czeslaw Bylinski.
Partial functions.
*Journal of Formalized Mathematics*, 1, 1989. - [6]
Czeslaw Bylinski.
Some basic properties of sets.
*Journal of Formalized Mathematics*, 1, 1989. - [7]
Malgorzata Korolkiewicz.
Homomorphisms of many sorted algebras.
*Journal of Formalized Mathematics*, 6, 1994. - [8]
Beata Madras.
Product of family of universal algebras.
*Journal of Formalized Mathematics*, 5, 1993. - [9]
Andrzej Trybulec.
Tarski Grothendieck set theory.
*Journal of Formalized Mathematics*, Axiomatics, 1989. - [10]
Andrzej Trybulec.
Many-sorted sets.
*Journal of Formalized Mathematics*, 5, 1993. - [11]
Andrzej Trybulec.
Many sorted algebras.
*Journal of Formalized Mathematics*, 6, 1994. - [12]
Andrzej Trybulec.
Categories without uniqueness of \rm cod and \rm dom.
*Journal of Formalized Mathematics*, 7, 1995. - [13]
Andrzej Trybulec.
Examples of category structures.
*Journal of Formalized Mathematics*, 8, 1996. - [14]
Andrzej Trybulec.
Functors for alternative categories.
*Journal of Formalized Mathematics*, 8, 1996. - [15]
Zinaida Trybulec.
Properties of subsets.
*Journal of Formalized Mathematics*, 1, 1989. - [16]
Edmund Woronowicz.
Relations and their basic properties.
*Journal of Formalized Mathematics*, 1, 1989.

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