Options

Exercise 70 - Chapter 3

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

Previous Next

Comments

  • 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 \\)?
  • 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) \\]
  • 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?
  • 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.
  • 5.
    edited July 6

    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...
Sign In or Register to comment.