<abstract xmlns="http://www.w3.org/1999/xhtml"><p>In the first part of this article we formalize the concepts of terminal and initial object, categorical product [4] and natural transformation within a free-object category [1]. In particular, we show that this definition of natural transformation is equivalent to the standard definition [13]. Then we introduce the exponential object using its universal property and we show the isomorphism between the exponential object of categories and the functor category [12].</p></abstract>

In the first part of this article we formalize the concepts of terminal and initial object, categorical product [4] and natural transformation within a free-object category [1]. In particular, we show that this definition of natural transformation is equivalent to the standard definition [13]. Then we introduce the exponential object using its universal property and we show the isomorphism between the exponential object of categories and the functor category [12].

Exponential Objects

Via del Pero 102, 54038 Montignoso, Italy

Formalized Mathematics

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

{"article-title":"Exponential Objects"}

In the first part of this article we formalize the concepts of terminal and initial object, categorical product [4] and natural transformation within a...

Exponential Objects

Publicado en línea: 25 mar 2016

Páginas: 351 - 369

Recibido: 15 ago 2015

DOI: https://doi.org/10.1515/forma-2015-0028

Palabras clave
exponential objects, functor category, natural transformation

© 2015 Marco Riccardi, published by De Gruyter Open

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

Exponential Objects

Publicado en línea: 25 mar 2016

Páginas: 351 - 369

Recibido: 15 ago 2015

DOI: https://doi.org/10.1515/forma-2015-0028

Palabras claveexponential objects, functor category, natural transformation

© 2015 Marco Riccardi, published by De Gruyter Open

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

Palabras clave
exponential objects, functor category, natural transformation