#### Howdy, Stranger!

It looks like you're new here. If you want to get involved, click one of these buttons!

Options

# Exercise 70 - Chapter 3

edited June 2018

In Example 3.69, we discussed an adjunction between functors $$- \times B$$ and $$(−)^B$$. But we only said how these functors worked on objects: for any set $$X$$, they return sets $$X \times B$$ and $$X^B$$ respectively.

1. Given a morphism $$f : X \rightarrow Y$$, what morphism should $$- \times B : X \times B \rightarrow Y \times B$$ return?
2. Given a morphism $$f : X \rightarrow Y$$, what morphism should $$(−)^B : X^B \rightarrow Y^B$$ return?
3. Consider the function $$+ : \mathbb{N} \times \mathbb{N} \rightarrow \mathbb{N}$$, which sends $$(a, b) \mapsto a + b$$. Currying $$+$$, we get a certain function $$p : \mathbb{N} → \mathbb{N}^\mathbb{N}$$. What is $$p(3)$$?

• Options
1.

1) $$X \times B \rightarrow Y \times B$$

2) $$X^B \rightarrow Y^B$$

3) $$+(-,3) = p(3)$$ where $$p(3): \mathbb{N} \rightarrow \mathbb{N}$$ and which sends $$(b) \mapsto 3 + b$$.

Does $$(X \rightarrow Y) \times B = X \times B \rightarrow Y \times B$$?

Does $$(X \rightarrow Y)^B = X^B \rightarrow Y^B$$?

Comment Source:1) \$$X \times B \rightarrow Y \times B \$$ 2) \$$X^B \rightarrow Y^B \$$ 3) \$$+(-,3) = p(3) \$$ where \$$p(3): \mathbb{N} \rightarrow \mathbb{N} \$$ and which sends \$$(b) \mapsto 3 + b \$$. Does \$$(X \rightarrow Y) \times B = X \times B \rightarrow Y \times B \$$? Does \$$(X \rightarrow Y)^B = X^B \rightarrow Y^B \$$? 
• Options
2.

Does $$(X \rightarrow Y) \times B = X \times B \rightarrow Y \times B$$?

Not in general, no. Not even for any Cartesian Closed Domain.

Does $$(X \rightarrow Y)^B = X^B \rightarrow Y^B$$?

Not in general, no. Not even for any Cartesian Closed Domain.

However, in a Cartesian Closed Domain we do have:

$(X \to Y)^B \cong X \to (Y^B)$

Comment Source:> Does \$$(X \rightarrow Y) \times B = X \times B \rightarrow Y \times B \$$? Not in general, no. Not even for any Cartesian Closed Domain. > Does \$$(X \rightarrow Y)^B = X^B \rightarrow Y^B \$$? Not in general, no. Not even for any Cartesian Closed Domain. ---------------------- However, in a Cartesian Closed Domain we **do** have: \$(X \to Y)^B \cong X \to (Y^B) \$
• Options
3.

Then I am lost on what to do with (1) and (2). Do you have any insight?

Comment Source:Then I am lost on what to do with (1) and (2). Do you have any insight?
• Options
4.

(1) should map $$f \mapsto \langle f, id\rangle$$

(2) should map $$f \mapsto \lambda g. f \circ g$$

If you don't mind some Haskell, Ralph Hinze and Daniel James have a nice paper Reason Isomorphically! (2010) that walks through all of these identities.

Comment Source:(1) should map \$$f \mapsto \langle f, id\rangle\$$ (2) should map \$$f \mapsto \lambda g. f \circ g\$$ If you don't mind some Haskell, Ralph Hinze and Daniel James have a nice paper [*Reason Isomorphically!* (2010)](http://www.cs.ox.ac.uk/ralf.hinze/publications/WGP10.pdf) that walks through all of these identities.
• Options
5.
edited July 2018

Matthew, but what is $$g$$ and $$\lambda$$ in (2)?

I tried the following, where $$F$$ stands for $$(-)^B$$:

• let B = 1, then we get $$X^1 \cong X$$ and $$F(f): x \mapsto (f(x))$$
• let B = 2, then we get $$X^2 \cong X \times X$$ and $$F(f): (x, x') \mapsto (f(x), f(x'))$$, or in other words $$F(f): X \times X \to Y\times Y$$, which in turn $$Y \times Y = Y^2$$
• for arbitrary B (even not finite), we get $$X^B \cong (X \times X \times ... \times X)_B$$, and therefore $$F(f): (x_1, x_2, ...) \mapsto (f(x_1), f(x_2), ...))$$

However, at the moment I don't know whether this makes sense and how to make it look better...

Comment Source:Matthew, but what is \$$g\$$ and \$$\lambda\$$ in (2)? I tried the following, where \$$F\$$ stands for \$$(-)^B\$$: - let B = 1, then we get \$$X^1 \cong X\$$ and \$$F(f): x \mapsto (f(x)) \$$ - let B = 2, then we get \$$X^2 \cong X \times X\$$ and \$$F(f): (x, x') \mapsto (f(x), f(x'))\$$, or in other words \$$F(f): X \times X \to Y\times Y\$$, which in turn \$$Y \times Y = Y^2\$$ - for arbitrary B (even not finite), we get \$$X^B \cong (X \times X \times ... \times X)_B \$$, and therefore \$$F(f): (x_1, x_2, ...) \mapsto (f(x_1), f(x_2), ...)) \$$ However, at the moment I don't know whether this makes sense and how to make it look better...
• Options
6.
edited August 2018

$$g$$ is an element of $$X^B$$, i.e., it is a function from $$B$$ to $$X$$. $$\lambda$$ is the lambda operator from the Lambda Calculus (which I know almost nothing about). So, 2), in words, says that $$f$$ maps to composition with $$f$$.

Edit: Maybe there is some way to look at composition with $$f$$ as what you were describing?

Comment Source:\$$g\$$ is an element of \$$X^B\$$, i.e., it is a function from \$$B\$$ to \$$X\$$. \$$\lambda\$$ is the lambda operator from the [Lambda Calculus](https://en.wikipedia.org/wiki/Lambda_calculus) (which I know almost nothing about). So, 2), in words, says that \$$f\$$ maps to composition with \$$f\$$. Edit: Maybe there is some way to look at composition with \$$f\$$ as what you were describing?