8
$\begingroup$

Suppose we're in a bicartesian closed category. Then given a morphism $$f : X \rightarrow Y_1 + \ldots + Y_n$$ and a test object $T$, we get a corresponding morphism $$T^f : X \times [Y_1,T] \times \ldots \times [Y_n,T] \rightarrow T.$$

Question. Does the morphism $T^f$ (and/or the transform $f \mapsto T^f$) have an accepted name, and where can I learn more about it?

Definition of $T^f$.

  1. Apply the functor $[-,T]$ to $f$, obtaining an arrow $[Y_1 + \ldots + Y_n, T] \rightarrow [X,T].$

  2. Move the $X$ back into its original position, obtaining an arrow $X \times [Y_1 + \ldots + Y_n, T] \rightarrow T.$

  3. Distribute the exponenial over the coproduct, obtaining an arrow $X \times [Y_1,T] \times \ldots \times [Y_n,T] \rightarrow T,$ as desired.

Remark 1. I think this transform is what allows modern programming languages to offer programmers such rubbish facilities for working with coproducts, while still allowing us to program essentially anything we want. For example, if we apply the coproduct-elimination transform to the function $\mathbf{Bool} \rightarrow 1 + 1$ and simplify just a little bit, we get a function $\mathbf{Bool} \times T \times T \rightarrow T.$ Now think of $T$ as the set of all valid command sequences in a programming language such as JavaScript, and notice how this gives us the general 'shape' of expressions of the following form:

if (x < y) {
  do_foo
} else {
  do_bar
}

Remark 2. Let $Y := Y_1 + \ldots + Y_n$. I claim that $f : X \rightarrow Y$ can be recovered from the map $(T \mapsto T^f)$. To see this, evaluate at $Y$. We end up with $Y^f : X \times [Y_1,Y] \times \cdots \times [Y_n,Y] \rightarrow Y$. Now use partial evaluation at the canonical elements of $[Y_i,Y]$, namely the inclusions. This should recover the original morphism.

Improve this question
$\endgroup$
5
  • 1
    $\begingroup$ This looks like one of the many manifestations of "strength" of a functor, which was first investigated by Anders Kock. As for a name, strong/strength are words that have been vastly over-used already. Look up Kock's work, but just describe your construction as what it does - don't give it a confusing name. $\endgroup$
    – Paul Taylor
    Commented Jul 25, 2020 at 8:43
  • 1
    $\begingroup$ @PaulTaylor, honestly I don't quite see the connection with functorial strengths. As I understand it, a strength allows you to take something outside a functor's arguments, and put it inside the arguments. Like so: $X \times FY \rightarrow F(X \times Y)$. But I can't really see the connection to what I'm asking.... $\endgroup$
    – goblin GONE
    Commented Jul 25, 2020 at 10:07
  • 3
    $\begingroup$ That is the version of "strength" that is commonly seen in the CS literature, especially since Eugenio Moggi's work. Kock investigated other forms, of which I suspect the original one was that the action of the functor on hom-sets $T:C(X,Y)\to D(T X,D Y)$ extends to internal homs $[X\to Y]\to[T X\to T Y]$ or $Y^X\to (T Y)^{(T X)}$. Kock did this for monoidal-closed categories; it's hardly worth mentioning for CCCs. His webpage is users-math.au.dk/kock $\endgroup$
    – Paul Taylor
    Commented Jul 25, 2020 at 13:19
  • 1
    $\begingroup$ $D Y$ above should of course have been $T Y$. Also, Kock wrote $[X\pitchfork Y]$ for the internal hom more recognisably called $[X\to Y]$. $\endgroup$
    – Paul Taylor
    Commented Jul 25, 2020 at 14:18
  • 1
    $\begingroup$ This transformation is also related, by way of propositions-as-types/Curry-Howard, to the DeMorgan laws of propositional logics, and for similar reasons to “continuation passing”. $\endgroup$
    – Ptharien's Flame
    Commented Jul 26, 2020 at 2:36

0

Reset to default

You must log in to answer this question.