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

- All Categories 2.4K
- Chat 502
- Study Groups 21
- Petri Nets 9
- Epidemiology 4
- Leaf Modeling 2
- Review Sections 9
- MIT 2020: Programming with Categories 51
- MIT 2020: Lectures 20
- MIT 2020: Exercises 25
- Baez ACT 2019: Online Course 339
- Baez ACT 2019: Lectures 79
- Baez ACT 2019: Exercises 149
- Baez ACT 2019: Chat 50
- UCR ACT Seminar 4
- General 73
- Azimuth Code Project 110
- Statistical methods 4
- Drafts 10
- Math Syntax Demos 15
- Wiki - Latest Changes 3
- Strategy 113
- Azimuth Project 1.1K
- - Spam 1
- News and Information 148
- Azimuth Blog 149
- - Conventions and Policies 21
- - Questions 43
- Azimuth Wiki 718

Options

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.

- Given a morphism \(f : X \rightarrow Y\), what morphism should \( - \times B : X \times B \rightarrow Y \times B \) return?
- Given a morphism \(f : X \rightarrow Y\), what morphism should \( (−)^B : X^B \rightarrow Y^B \) return?
- 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)\)?

## Comments

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 \)?

`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 \\)?`

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

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

However, in a Cartesian Closed Domain we

dohave:\[ (X \to Y)^B \cong X \to (Y^B) \]

`> 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) \\]`

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

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

(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.`(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.`

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

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

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

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

\(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?

`\\(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?`