> For the complete documentation index, see [llms.txt](https://mandober.gitbook.io/math-debrief/llms.txt). Markdown versions of documentation pages are available by appending `.md` to page URLs; this page is available as [Markdown](https://mandober.gitbook.io/math-debrief/450-category-theory/terms/function-type.md).

# Function type

<https://bartoszmilewski.com/2015/03/13/function-types/>

A function type is different from other types: Int, for instance, is just a set of integers, Bool is a two element set, but a function type `a -> b` is more than that: it is a set of morphisms between objects `a` and `b`. A set of morphisms between two objects in any category is called a *hom-set*. It just so happens that in the category `𝗦𝗲𝘁` every hom-set is itself an object in the same category because it is, after all, a set. The same is not true of other categories where hom-sets are external to a category. They are even called *external hom-sets*. It is the self-referential nature of the category `𝗦𝗲𝘁` that makes function types special. But there is a way, at least in some categories, to construct objects that represent hom-sets. Such objects are called *internal hom-sets*.

## Universal Construction

Let's forget for a moment that function types are sets and try to construct a function type, or more generally, an internal hom-set, from scratch. As usual, we'll take our cues from the Set category, but carefully avoid using any properties of sets, so that the construction will automatically work for other categories.

A function type may be considered a composite type because of its relation to the argument type and the result type. We've already seen the constructions of composite types - those that involved relations between objects. We used universal constructions to define a product type and a coproduct types. We can use the same approach to define a function type: we need a pattern that involves 3 objects: 1. the function type that we're constructing, `a -> b` 2. the argument type, `a` 3. the result type, `b`

The obvious pattern that connects these three types is called *function application*. Given a candidate for a function type, let's call it `z` (notice that, if we are not in the category Set, this is just an object like any other object), and the argument type `a` (an object), the application maps this pair to the result type `b` (an object). Similar to modus ponens: `a -> b, a |- b`.

app :: ⟨a -> b, a⟩ ⟼ b

So, we have 3 objects, and two of them are fixed (those representing the argument type and the result type).

We also have the application, which is a mapping. How do we incorporate this mapping into our pattern? If we were allowed to look inside objects, we could pair a function `f ∈ z` with an argument `x ∈ a` and map it to `f x ∈ b`.

In the `𝗦𝗲𝘁` category, we can pick a function `f` from a set of functions `z`, and we can pick an argument `x` from the set/type `a`, and we get an element `f x` in the set/type `b`.

But instead of dealing with individual pairs (f, x), we can talk about the whole product of the function type z and the argument type a. The product `z×a` is an object, and we can pick, as our application morphism, an arrow `g` from that object to `b`. In Set, `g` would be the function that maps every pair `(f, x)` to `f x`.

That is our pattern: a product of two objects `z` and `a`, linked to another object `b` by a morphism `g`.

z × a ----g---> b