Displaying similar documents to “Characterizations of Lambek-Carlitz type”

Exponential Objects

Marco Riccardi (2015)

Formalized Mathematics

Similarity:

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].