<abstract xmlns="http://www.w3.org/1999/xhtml"><p>The main purpose of this article is to introduce the categorical concept of pullback in Mizar. In the first part of this article we redefine homsets, monomorphisms, epimorpshisms and isomorphisms [7] within a free-object category [1] and it is shown there that ordinal numbers can be considered as categories. Then the pullback is introduced in terms of its universal property and the Pullback Lemma is formalized [15]. In the last part of the article we formalize the pullback of functors [14] and it is also shown that it is not possible to write an equivalent definition in the context of the previous Mizar formalization of category theory [8].</p></abstract>

The main purpose of this article is to introduce the categorical concept of pullback in Mizar. In the first part of this article we redefine homsets, monomorphisms, epimorpshisms and isomorphisms [7] within a free-object category [1] and it is shown there that ordinal numbers can be considered as categories. Then the pullback is introduced in terms of its universal property and the Pullback Lemma is formalized [15]. In the last part of the article we formalize the pullback of functors [14] and it is also shown that it is not possible to write an equivalent definition in the context of the previous Mizar formalization of category theory [8].

Categorical Pullbacks

Via del Pero 102, 54038 Montignoso, Italy

Formalized Mathematics

This work is licensed under the Creative Commons Attribution-ShareAlike 3.0 License.

{"article-title":"Categorical Pullbacks"}

The main purpose of this article is to introduce the categorical concept of pullback in Mizar. In the first part of this article we redefine homsets,...

Categorical Pullbacks

Online veröffentlicht: 31. März 2015

Seitenbereich: 1 - 14

Eingereicht: 31. Dez. 2014

DOI: https://doi.org/10.2478/forma-2015-0001

Schlüsselwörter
category pullback, pullback lemma

© Marco Riccardi

This work is licensed under the Creative Commons Attribution-ShareAlike 3.0 License.

Categorical Pullbacks

Online veröffentlicht: 31. März 2015

Seitenbereich: 1 - 14

Eingereicht: 31. Dez. 2014

DOI: https://doi.org/10.2478/forma-2015-0001

Schlüsselwörtercategory pullback, pullback lemma

© Marco Riccardi

This work is licensed under the Creative Commons Attribution-ShareAlike 3.0 License.

Schlüsselwörter
category pullback, pullback lemma