Proszę używać tego identyfikatora do cytowań lub wstaw link do tej pozycji:
Pełny rekord metadanych
Pole DCWartośćJęzyk
dc.contributor.authorRiccardi, Marcopl
dc.identifier.citationFormalized Mathematics, Volume 23, Issue 1, Pages 1–14pl
dc.description.abstractThe 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].pl
dc.publisherDe Gruyter Openpl
dc.subjectpullback lemmapl
dc.subjectcategory pullbackpl
dc.titleCategorical Pullbackspl
dc.description.AffiliationVia del Pero 102, 54038 Montignoso, Italypl
dc.description.referencesJiri Adamek, Horst Herrlich, and George E. Strecker. Abstract and Concrete Categories: The Joy of Cats. Dover Publication, New York,
dc.description.referencesGrzegorz Bancerek. Cardinal numbers. Formalized Mathematics, 1(2):377–382,
dc.description.referencesGrzegorz Bancerek. The ordinal numbers. Formalized Mathematics, 1(1):91–96,
dc.description.referencesGrzegorz Bancerek. The well ordering relations. Formalized Mathematics, 1(1):123–129,
dc.description.referencesGrzegorz Bancerek. Zermelo theorem and axiom of choice. Formalized Mathematics, 1 (2):265–267,
dc.description.referencesGrzegorz Bancerek and Krzysztof Hryniewiecki. Segments of natural numbers and finite sequences. Formalized Mathematics, 1(1):107–114,
dc.description.referencesFrancis Borceaux. Handbook of Categorical Algebra I. Basic Category Theory, volume 50 of Encyclopedia of Mathematics and its Applications. Cambridge University Press, Cambridge,
dc.description.referencesCzesław Byliński. Introduction to categories and functors. Formalized Mathematics, 1 (2):409–420,
dc.description.referencesCzesław Byliński. Functions and their basic properties. Formalized Mathematics, 1(1): 55–65,
dc.description.referencesCzesław Byliński. Functions from a set to a set. Formalized Mathematics, 1(1):153–164,
dc.description.referencesCzesław Byliński. Partial functions. Formalized Mathematics, 1(2):357–367,
dc.description.referencesCzesław Byliński. Some basic properties of sets. Formalized Mathematics, 1(1):47–53,
dc.description.referencesAgata Darmochwał. Finite sets. Formalized Mathematics, 1(1):165–167,
dc.description.referencesF. William Lawvere. Functorial semantics of algebraic theories and some algebraic problems in the context of functorial semantics of algebraic theories. Reprints in Theory and Applications of Categories, 5:1–121,
dc.description.referencesSaunders Mac Lane. Categories for the Working Mathematician, volume 5 of Graduate Texts in Mathematics. Springer Verlag, New York, Heidelberg, Berlin,
dc.description.referencesBeata Padlewska. Families of sets. Formalized Mathematics, 1(1):147–152,
dc.description.referencesMarco Riccardi. Object-free definition of categories. Formalized Mathematics, 21(3): 193–205, 2013. doi:10.2478/
dc.description.referencesAndrzej Trybulec. Enumerated sets. Formalized Mathematics, 1(1):25–34,
dc.description.referencesZinaida Trybulec. Properties of subsets. Formalized Mathematics, 1(1):67–71,
dc.description.referencesEdmund Woronowicz. Relations and their basic properties. Formalized Mathematics, 1 (1):73–83,
dc.description.referencesEdmund Woronowicz. Relations defined on sets. Formalized Mathematics, 1(1):181–186,
Występuje w kolekcji(ach):Formalized Mathematics, 2015, Volume 23, Issue 1

Pliki w tej pozycji:
Plik Opis RozmiarFormat 
forma-2015-0001.pdf272,78 kBAdobe PDFOtwórz
Pokaż uproszczony widok rekordu Zobacz statystyki

Pozycja ta dostępna jest na podstawie licencji Licencja Creative Commons CCL Creative Commons