@MISC{CAT_7.MIZ,
  AUTHOR = {Riccardi, Marco},
  TITLE = {Categorical Pullbacks},
  SECTION1 = {Preliminaries},
  SECTION2 = {Hom-sets},
  SECTION3 = {Monomorphisms, Epimorphisms and Isomorphisms},
  SECTION4 = {Ordinal Numbers as Categories},
  SECTION5 = {Pullbacks},
  SECTION6 = {Pullbacks of Functors},
  DAY = {31},
  MONTH = {December},
  YEAR = {2014},
  ADDRESS1 = {Via del Pero 102\\54038 Montignoso\\Italy},
  SUMMARY = {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 hom-sets, monomorphisms,
  epimorpshisms and isomorphisms \cite{Borceaux} within a free-object category \cite{CAT_6.ABS} 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.
  In the last part of the article we formalize the pullback of functors \cite{Lawvere:1963} 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 \cite{CAT_1.ABS}.}}

@BOOK{Borceaux,
       AUTHOR = {Borceaux, Francis},
        TITLE = {Handbook of Categorical Algebra I. {B}asic Category Theory},
    PUBLISHER = {Cambridge University Press},
         YEAR = {1994},
       VOLUME = {50},
       SERIES = {Encyclopedia of Mathematics and its Applications},
      ADDRESS = {Cambridge}}

@ARTICLE{Lawvere:1963,
       AUTHOR = {Lawvere, F. William},
        TITLE = {Functorial Semantics of Algebraic Theories and
                 Some Algebraic Problems in the context of Functorial Semantics of Algebraic Theories},
      JOURNAL = {Reprints in Theory and Applications of Categories},
         YEAR = {2004},
       VOLUME = {5},
        PAGES = {1--121}}
