Added a reference to a paper of Pavelka.

]]>I noticed that it would be more natural to define closed categories without assuming a category from the outset, and then I realised Mike had already suggested this back in #22 :) It reminds me somewhat of the fact that a relative monad can be defined in terms only of an object-function, and functoriality derived from the extension operator.

Did anything ever come of this? It would be nice for it to be written out in the literature.

]]>added DOI-link for:

- Samuel Eilenberg, Max Kelly,
*Closed categories*, Proc. Conf. Categorical Algebra (La Jolla, Calif., 1965), Springer (1966) [doi:10.1007/978-3-642-99902-4_22]

Mention right-closed categories.

]]>$L^x_{y,z}$. Other categories doesn't allow opposite category. For example the category of Sets or Additive groups.

We can add two functions $+g$ if we have addition in target space, but not in source space.

So the category can be closed wih mappings $L^x_{y,z} $ without having defined mappings $R^x_{y,z}$.

Interesting closed category is provided by uniform mappings of uniform spaces. ]]>

Added remark that a *symmetric* closed category is automatically associative as a promonoidal category, hence a weaker representability condition suffices to make it monoidal.

Added one axiom to prounital closed categories.

]]>Added link to published version of Oleksandr Manzyuk, _Closed categories vs. closed multicategories (TAC Vol. 26, 2012). Hope I got your formatting schemes not too messed up!

]]>Change “semi-closed category” to “prounital closed category”

]]>You mean a multicategory where there are universal binary maps $A,B \to A\otimes B$ but not a universal nullary map $\cdot \to I$?

Yes, that’s what I meant. Since that’s the monoidal analogue of prounital closed categories, which (conjecturally) correspond to multicategories that have nullary *maps*, but have a “binary internal-hom” but not a “nullary one”.

“prounital”?

Sounds good to me!

There’s no name for a multicategory that has binary tensor products but not a unit, either.

You mean a multicategory where there are universal binary maps $A,B \to A\otimes B$ but not a universal nullary map $\cdot \to I$? I don’t know a name for that, but I think the multicategory equivalent of a semigroup category is a multicategory with no nullary operations that is representable in the standard sense, so “representable constantless multicategory” (adopting the terminology you suggested before), or “representable non-unitary multicategory” (using Fresse’s terminology for the corresponding operads, which I don’t find particularly evocative).

]]>“prounital”?

]]>Hrm, I suppose you’re right. There’s no name for a multicategory that has binary tensor products but not a unit, either.

]]>Re #41, I wouldn’t call these “semi-closed categories” since that name has already been used by Bourke (#16) for the weaker structure consisting of just a bifunctor $[-,-] : C^{op} \times C \to C$ equipped with the compositor transformations $[Y,Z] \to [[X,Y],[X,Z]]$ satisfying a pentagon axiom. And as you know (#17), that terminology is natural because such semi-closed categories indeed correspond to (biased-lax/skew) semigroups in $Prof$ with a representability requirement.

What’s tricky here is that a “non-unital” closed category *is* actually equipped with a unit (in $Prof$), it is just not representable. I’m not sure if there is a succinct way of conveying that…perhaps something like a “semi-closed category with a presheaf of global elements”?

I suppose a better name for “non-unital closed categories” would be “semi-closed categories”, by analogy to other uses of “semi-” for non-unitality (e.g. semigroup, semisimplicial set, semicategory…)

]]>List some examples of closed monoidal categories whose closed structure is more natural than their monoidal structure.

]]>I don’t really understand all this skew business, and I’m not really motivated to put in the effort right now, since I don’t know or care about any of the relevant examples yet, and from a pure category-theoretic point of view it seems bizarre to me to have the unit morphisms pointing in different directions. (Even more bizarre than a noninvertible biased associator.) I accept that they *do* arise naturally in some contexts and *are* useful for some purposes, but the correspondence between non-unital closed categories and closed multicategories seems to me something much more basic, that should be simple to motivate, explain, and prove, without having to descend into this more exotic skew business.

By the way, I think you meant $M : C^{op}\times C^{op}\times C\to Set$.

Oops…I mean, that was just to prove my point that keeping track of all the directions/signs can be tricky! :-)

]]>Those are the same as my calculations: it’s just that since $\lambda$ is an isomorphism, it could just as well point the other way. The reason I think it

shouldpoint the other way is because the criterion of correctness for the definition should be that it coincides with closed multicategories, and we know that multicategories can be identified with normal unbiased lax monoids in $Prof$.

Hmm. It’s subtle, but I have a different intuition. Or I guess it’s rather that I don’t want to start from an assumption of left normality. I think the notion of “skew” multicategory discussed by Bourke and Lack is quite natural, and there, what corresponds to the left unitor is the mapping from “tight” morphisms $A_0;A_1,\dots,A_n \to B$ to “loose” morphisms $A_0,A_1,\dots,A_n \to B$. My intuition coming from programming languages is that this corresponds to an inclusion of (“pure”) values into (“effectful”) computations, and so I think it will be interesting to consider closed skew multicategories which are not left normal (corresponding to extensions of the lambda calculus with effects). That is quite informal intuition, though.

In any case, I wanted to elaborate a bit more formally what I was alluding to at the end of #29, because I think it might be related to your ideas in #22, and possibly to this question of left normality. Given a (unital or non-unital, not necessarily left normal) skew closed category $C$, we can consider its category of covariant presheaves $[C,Set]$ as a right-skew monoidal category (or alternatively $[C,Set]^{op}$ as a left-skew monoidal category of course). Then it is interesting to consider _monoids_in $[C,Set]$, which correspond to “deductively closed presheaves” $R : C \to Set$, in the sense that the multiplication map gives an extranatural transformation

$m : R(a \to b) \times R(a) \to R(b)$corresponding to “modus ponens”, while the unit gives a natural transformation

$u : U(a) \to R(a)$corresponding to the inclusion of all “tautologies” into $R$.

Let me restrict now to the unital, 2-enriched case, because that’s what I considered in the aforementioned paper (but I think it can be extended to the non-unital, Set-enriched case). In this case, a monoid $R$ in $[C,2]$ (where $C$ is a unital skew closed preorder) corresponds to an upwards closed subset of $C$ such that the following pair of conditions hold:

$\frac{a \to b \in R \quad a \in R}{b \in R} \qquad \frac{}{I \in R}$Given such a monoid, we can construct a new preordered category $C/R = (C,\le_R)$ with the same objects as $C$ but where $a \le_R b$ iff $a\to b \in R$. The fact that this relation is transitive relies on both the multiplication $m$ of $R$ and the original associator $\alpha$/compositor $L$ of $C$, while the fact that it is reflexive relies on the unit $u$ of $R$ together with the left unitor $\lambda$ of $C$. There is also an evident embedding $i : C \to C/R$ (again relying on the left unitor $\lambda$), in the sense that the preorder $\le_R$ is an extension of $\le$.

But now we might wonder whether $C/R$ is (skew) closed, and whether we can legitimately see it as a quotient. And here is where things get more interesting: although we can show that the original operation $a\to b$ is monotone in $b$ relative to the coarser order $\le_R$, it need not be antitone in $a$. So this is where we need to impose an additional condition of closure under “double-negation introduction”:

$\frac{a \in R}{(a \to b) \to b \in R}$Note that this dni-condition is equivalent (at least in the 2-enriched case) to the existence of a natural transformation $-\otimes R \Rightarrow R\otimes-$, where $\otimes$ is the multiplication operation in $[C,2]$. Given this additional closure condition, we can prove that $a \to b$ is antitone in $a$ relative to $\le_R$ and thus defines a functor $(C/R)^{op} \times C/R \to C/R$, which together with the original unit $I$ turns $C/R$ into a *left normal* skew-closed category. Moreover we can show that $(C/R, i : C \to C/R)$ has the appropriate universal property of the quotient.

I did not try to work this out, but my intuition was that in the $Set$-enriched case, $R$ could be thought of as (generated by) a family of typed combinators, which is then used to construct a closed category $C_R$ with additional structure. Perhaps that aligns with some of your ideas?

]]>By the way, I think you meant $M : C^{op}\times C^{op}\times C\to Set$.

I think I see the point now that viewing them as left-normal skew monoids, whose corresponding LBC-algebras are also left-normal and hence equivalently left-normal lax monoids, would make the identification of non-unital closed categories with closed multicategories literally a consequence of Bourke-Lack rather than requiring the argument to be redone in the biased-lax case. Morally I still think the latter ought to be done, though… but I might be too lazy to do it.

]]>Those are the same as my calculations: it’s just that since $\lambda$ is an isomorphism, it could just as well point the other way. The reason I think it *should* point the other way is because the criterion of correctness for the definition should be that it coincides with closed multicategories, and we know that multicategories can be identified with normal unbiased lax monoids in $Prof$.

Pondering a bit more what you are saying and trying to connect it to things that I know, I think that the definition of “non-unital closed category” you are aiming for should begin with a *skew* monoid in $Prof$ (like I was suggesting in #21) rather than a biased lax monoid. Keeping track of the directions can be tricky (nice table at lax monoidal category, by the way!), so let me spell out my calculations.

Start with a right-skew monoid $(A, M : A \otimes A ⇸ A, U : 1 ⇸ A, \alpha, \lambda, \rho)$ in $Prof$, where we write $A = C^{op}$ for the opposite of some (non-unital closed) category $C$, so that $M$ and $U$ correspond to functors $M : C \times C \times C^{op} \to Set$ and $U : C \to Set$. Now we ask that $M$ is representable by a functor $[-,-] : C^{op} \times C \to C$ in the sense that

$M(c,a;b) = C(c,[a,b])$By profunctor composition the two halves of associativity $L = M(M(-,-),-)$ and $R = M(-,M(-,-))$ are calculated as follows

$L(d,e,a;c) = \int^b C(d, [e,b]) \times C(b, [a,c]) \cong C(d,[e,[a,c]]) \qquad R(d,e,a;c) = \int^b C(d,[b,c]) \times C(e,[a,b])$so that the right-to-left associator $\alpha : R \Rightarrow L$ yields the family of “compositor” maps

$L_{b,c}^a : [b,c] \to [[a,b],[a,c]]$in $C$. Now, consider the profunctors $U_L = M(U,-)$ and $U_R = M(-,U)$. I calculate them as follows:

$U_L(a;b) = \int^c U(c) \times C(c,[a,b]) \cong U([a,b]) \qquad U_R(c;b) = \int^a C(c,[a,b]) \times U(a)$Therefore the left unitor $\lambda : A \Rightarrow U_L$ corresponds to a transformation

$C(a,b) \to U([a,b])$while the right unitor $\rho : U_R \Rightarrow A$ corresponds to a transformation

$U(a) \to C([a,b],b)$So this is what one could call a “non-unital skew closed category”. If you additionally impose that $\lambda$ is an isomorphism (= left normality) then I think what comes out is what you are calling a “non-unital closed category”.

]]>Ah, nice! I thought there might be some argument like that, but I didn’t see it.

]]>Re: #29, are you saying that with only the “evaluation” operation he is able to get the functoriality rule somehow?

Yes. (And I proved something similar as Prop. 2.23 in the above link.) The key is to prove the following rule as a lemma (in the notation of #28):

$\frac{A \to B}{(B \to C) \to (A \to C)}$Proof: Assume $A \to B$. By the “evaluation”/”dni” rule, we have $((A \to B) \to (A \to C)) \to (A \to C)$ (taking $A \to C$ as the “answer type” of double-negation introduction). Composing this with the “B” axiom $(B\to C) \to ((A \to B) \to (A \to C))$, we obtain $(B \to C) \to (A \to C)$. (Here I am using the auxiliary lemma that it is possible to compose a deduction $f : X \to Y$ with a deduction $g : Y \to Z$ to obtain a deduction $h : X \to Z$: first we apply modus ponens on the axiom $(Y \to Z) \to ((X \to Y) \to (X \to Z))$ together with $g$ to obtain a deduction $g' : ((X \to Y) \to (X \to Z))$, then we apply modus ponens on $g'$ with $f$ to obtain $h : X \to Z$.)

Now we can derive the functoriality rule

$\frac{A_2 \to A_1 \quad B_1 \to B_2}{(A_1 \to B_1) \to (A_2 \to B_2)}$as follows. Suppose given $f : A_2 \to A_1$ and $g : B_1 \to B_2$. First we apply modus ponens on the B axiom and $g$ to obtain $g' : (A_2 \to B_1) \to (A_2 \to B_2)$. Then we apply the lemma to $f$ to obtain $f' : (A_1 \to B_1) \to (A_2 \to B_1)$. Finally we compose $f'$ and $g'$ to obtain the desired $h : (A_1 \to B_1) \to (A_2 \to B_2)$.

]]>