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

- All Categories 2.2K
- Programming with Categories Course 21
- Exercises - Programming with Categories Course 15
- Applied Category Theory Course 341
- Applied Category Theory Seminar 4
- Exercises - Applied Category Theory Course 149
- Discussion Groups 50
- How to Use MathJax 15
- Chat 487
- Azimuth Code Project 108
- News and Information 147
- Azimuth Blog 149
- Azimuth Forum 29
- Azimuth Project 189
- - Strategy 108
- - Conventions and Policies 21
- - Questions 43
- Azimuth Wiki 711
- - Latest Changes 701
- - - Action 14
- - - Biodiversity 8
- - - Books 2
- - - Carbon 9
- - - Computational methods 38
- - - Climate 53
- - - Earth science 23
- - - Ecology 43
- - - Energy 29
- - - Experiments 30
- - - Geoengineering 0
- - - Mathematical methods 69
- - - Meta 9
- - - Methodology 16
- - - Natural resources 7
- - - Oceans 4
- - - Organizations 34
- - - People 6
- - - Publishing 4
- - - Reports 3
- - - Software 21
- - - Statistical methods 2
- - - Sustainability 4
- - - Things to do 2
- - - Visualisation 1
- General 41

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