Volume 3, 1991

University of Bialystok

Copyright (c) 1991 Association of Mizar Users

**Czeslaw Bylinski**- Warsaw University, Bialystok

- If $V$ is any non-empty set of sets, we define $\hbox{\bf Ens}_V$ to be the category with the objects of all sets $X \in V$, morphisms of all mappings from $X$ into $Y$, with the usual composition of mappings. By a mapping we mean a triple $\langle X,Y,f \rangle$ where $f$ is a function from $X$ into $Y$. The notations and concepts included corresponds to that presented in [12], [10]. We also introduce representable functors to illustrate properties of the category {\bf Ens}.

- Mappings
- Category Ens
- Representable Functors

- [1]
Grzegorz Bancerek.
Curried and uncurried functions.
*Journal of Formalized Mathematics*, 2, 1990. - [2]
Czeslaw Bylinski.
Functions and their basic properties.
*Journal of Formalized Mathematics*, 1, 1989. - [3]
Czeslaw Bylinski.
Functions from a set to a set.
*Journal of Formalized Mathematics*, 1, 1989. - [4]
Czeslaw Bylinski.
Introduction to categories and functors.
*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]
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. - [8]
Czeslaw Bylinski.
Subcategories and products of categories.
*Journal of Formalized Mathematics*, 2, 1990. - [9]
Czeslaw Bylinski.
Opposite categories and contravariant functors.
*Journal of Formalized Mathematics*, 3, 1991. - [10] Saunders Mac Lane. \em Categories for the Working Mathematician, volume 5 of \em Graduate Texts in Mathematics. Springer Verlag, New York, Heidelberg, Berlin, 1971.
- [11]
Bogdan Nowak and Grzegorz Bancerek.
Universal classes.
*Journal of Formalized Mathematics*, 2, 1990. - [12] Zbigniew Semadeni and Antoni Wiweger. \em Wst\c ep do teorii kategorii i funktorow, volume 45 of \em Biblioteka Matematyczna. PWN, Warszawa, 1978.
- [13]
Andrzej Trybulec.
Binary operations applied to functions.
*Journal of Formalized Mathematics*, 1, 1989. - [14]
Andrzej Trybulec.
Domains and their Cartesian products.
*Journal of Formalized Mathematics*, 1, 1989. - [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]
Zinaida Trybulec.
Properties of subsets.
*Journal of Formalized Mathematics*, 1, 1989. - [19]
Edmund Woronowicz.
Relations and their basic properties.
*Journal of Formalized Mathematics*, 1, 1989.

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