4
$\begingroup$

Let $\mathcal{C}$ be a category, with terminal object $1$ but where not all products necessarily exist, and consider the following definition:

Given objects $A,B$, we say that $A^B$ together with a morphism $\epsilon : B \times A^B\to A$ is a weak exponential object if for every morphism $f \in \mathrm{Hom}(B,A)$ there exists a unique morphism $[f] \in \mathrm{Hom}(1,A^B)$ such that for all $x \in \mathrm{Hom}(1,B)$ we have $ \epsilon \circ \langle x, [f]\rangle=f \circ x $.

For some context, I came up with this definition while trying to answer the question: Given some finitely generated category $\mathcal{C}$ (i.e. the quotient of some free category generated by a finite graph), is there some (concrete) construction we can describe which freely adjoins exponential objects to the category (constructing the free Cartesian closed category containing $\mathcal{C}$)?

Of course, this is rather difficult, at least on the face of it, since the usual definition of exponential object requires the category $\mathcal{C}$ already contain all finite products -- but also must adjoin new products (e.x. $A \times B^A$) to the category at the same time as adjoining the new exponential objects. So my motivation for this definition was to try to separate this dependence somewhat to make my construction easier.

However, I'm not entirely sure what the nature of this sort of "weak exponential object" is. Has such a notion been considered before in the literature? If so, is it known how this definition relates to the usual notion of an exponential object? (Me calling this a "weak" exponential object somewhat begs the question, but it seems to me this should not be as general as the usual notion of an exponential object -- since how to define the exponential transpose from this definition of mine is not clear, even if $\mathcal{C}$ has all finite products.)

$\endgroup$
  • $\begingroup$ I edited two typos but also changed the universal property of evaluation to what it usually is-your original version didn't type check, as $x\times [f]: 1\to A^B$ when you need $B\to B\times A^B$, but maybe you meant some third option? If I've got you right, then I think any poset with a top and a bottom element has these weak exponentials, given by $1$ if $B\leq A$ and $0$ if not. $\endgroup$ – Kevin Carlson Feb 2 '18 at 16:43
  • $\begingroup$ @kevinCarlson I looked at this again -- I think my mistake was that I intended $\langle x, [f] \rangle$, not $x \times [f]$, so this should make more sense now. $\endgroup$ – Nathan BeDell Feb 3 '18 at 17:44
1
$\begingroup$

It's hard to tell, but this looks similar to the $\zeta$-calculus as described in Hasegawa's Decomposing typed lambda calculus into a couple of categorical programming languages.

The idea is to split the lambda calculus into two calculi, the $\kappa$-calculus and the $\zeta$-calculus, the first capturing multi-parameter first-order functions and contextual completeness and the second capturing (single-parameter) higher-order functions and functional completeness.

The paper uses polynomial categories as a simpler variation on fibrations for talking about arrows in context. Given a category $\mathcal{C}$ with a terminal object, there is for each object $C$ of $\mathcal{C}$ another category $\mathcal{C}[x:C]$ which consists $\mathcal{C}$ with an arrow $x : 1\to C$ freely attached. We have the obvious (terminal object preserving) functor $I_{x:C}:\mathcal{C}\to\mathcal{C}[x:C]$ which satisfies the following universal property. Given a category $\mathcal{D}$ with terminal object, a terminal object preserving functor $F:\mathcal{C}\to\mathcal{D}$, and an arrow $c:F1\to FC$, there is a unique functor $F_c : \mathcal{C}[x:C]\to\mathcal{D}$ such that $F=F_c\circ I_{x:C}$ and $F_c(x)=c$. In particular, choosing $F=Id$ produces $Id_c :\mathcal{C}[x:C]\to\mathcal{C}$ which is called the substitution functor and also written post-fix as $-[c/x]$. We can, of course, iterate the polynomial category construction. The $\kappa$-calculus is what we get when we say all inclusions functors have left adjoints which are preserved by substitution functors. The $\zeta$-calculus is what we get when we say all inclusion functors have right adjoints which are preserved by substitution functors. Given both the $\kappa$-calculus and the $\zeta$-calculus, the adjunctions can be composed to produce a Cartesian closed category and the $\lambda$-calculus. This splitting is similar to the comprehension category based approached in Jacobs' Simply Typed and Untyped Lambda Calculus Revisited.

The adjunction gives a natural transformation $\mathcal{C}[x:C](I_{x:C}A,B)\to\mathcal{C}(A,B^C)$ which we can think of as "currying" the $C$ or binding $x$. The counit combined with substitution gives a notion of application. Given an arrow $c:1\to C$, we have an arrow $B^C\to B$. In terms of the lambda calculus, this is like restricting application to only apply closed terms to functions.

$\endgroup$
  • $\begingroup$ @DerikElkins, thanks for sharing this paper! This is a really interesting approach to treating arrows in context that I haven't seen before -- seems much more intuitive to me than the fibrational approach, anyway. I agree with you that the $\zeta$-calculus does seem like it is probably related to what I was trying to do here. $\endgroup$ – Nathan BeDell Feb 3 '18 at 18:08

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.