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:
Mention right-closed categories.
]]>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 but not a universal nullary map ?
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 but not a universal nullary map ? 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 equipped with the compositor transformations 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 with a representability requirement.
What’s tricky here is that a “non-unital” closed category is actually equipped with a unit (in ), 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 .
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 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 .
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 to “loose” morphisms . 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 , we can consider its category of covariant presheaves as a right-skew monoidal category (or alternatively as a left-skew monoidal category of course). Then it is interesting to consider _monoids_in , which correspond to “deductively closed presheaves” , in the sense that the multiplication map gives an extranatural transformation
corresponding to “modus ponens”, while the unit gives a natural transformation
corresponding to the inclusion of all “tautologies” into .
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 in (where is a unital skew closed preorder) corresponds to an upwards closed subset of such that the following pair of conditions hold:
Given such a monoid, we can construct a new preordered category with the same objects as but where iff . The fact that this relation is transitive relies on both the multiplication of and the original associator /compositor of , while the fact that it is reflexive relies on the unit of together with the left unitor of . There is also an evident embedding (again relying on the left unitor ), in the sense that the preorder is an extension of .
But now we might wonder whether 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 is monotone in relative to the coarser order , it need not be antitone in . So this is where we need to impose an additional condition of closure under “double-negation introduction”:
Note that this dni-condition is equivalent (at least in the 2-enriched case) to the existence of a natural transformation , where is the multiplication operation in . Given this additional closure condition, we can prove that is antitone in relative to and thus defines a functor , which together with the original unit turns into a left normal skew-closed category. Moreover we can show that has the appropriate universal property of the quotient.
I did not try to work this out, but my intuition was that in the -enriched case, could be thought of as (generated by) a family of typed combinators, which is then used to construct a closed category with additional structure. Perhaps that aligns with some of your ideas?
]]>By the way, I think you meant .
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 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 .
]]>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 (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 in , where we write for the opposite of some (non-unital closed) category , so that and correspond to functors and . Now we ask that is representable by a functor in the sense that
By profunctor composition the two halves of associativity and are calculated as follows
so that the right-to-left associator yields the family of “compositor” maps
in . Now, consider the profunctors and . I calculate them as follows:
Therefore the left unitor corresponds to a transformation
while the right unitor corresponds to a transformation
So this is what one could call a “non-unital skew closed category”. If you additionally impose that 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):
Proof: Assume . By the “evaluation”/”dni” rule, we have (taking as the “answer type” of double-negation introduction). Composing this with the “B” axiom , we obtain . (Here I am using the auxiliary lemma that it is possible to compose a deduction with a deduction to obtain a deduction : first we apply modus ponens on the axiom together with to obtain a deduction , then we apply modus ponens on with to obtain .)
Now we can derive the functoriality rule
as follows. Suppose given and . First we apply modus ponens on the B axiom and to obtain . Then we apply the lemma to to obtain . Finally we compose and to obtain the desired .
]]>