Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
1 to 18 of 18
Can anyone suggest a naturally-occurring monoidal category whose terminal object is not the unit of the monoidal structure and where also ?
What about , taking to be the coproduct?
Okay, yeah, of course, I simplified too much. How about a closed monoidal category with these properties?
A cheap response is to tweak Oscar’s example to , and pass to via Day convolution.
Why do you want to know? :-)
Here might be a “more natural” example: do the same as in the last comment, but with in place of , with its usual tensor product (corresponding to simplicial join). I.e., pass to simplicial sets with the induced tensor product.
Ah, good one: the join on augmented simplicial sets.
I’m thinking about substructural type theories for categories, such as a term calculus for intuitionistic linear logic (with ) that presents a free closed monoidal category with products and coproducts. And I noticed that the term for the unique inhabitant of (the additive truth, i.e. the terminal object) can’t be just “” the way it is in cartesian type theory, but has to take all the variables from the context as arguments. Otherwise a term like is ambiguous; we ought to write either or . But then I couldn’t think of any examples of a naturally-ocurring monoidal category where this difference actually mattered.
(Why am I thinking about this, you may ask? Because I’m preparing to teach a short course on categorical logic.)
Are you typing up notes to go with this? I’d enjoy seeing them.
Yes; in fact the notes seem to be turning into something quite extensive, and I haven’t even gotten to first-order logic yet. Here. I would welcome advance feedback, especially from category theorists on their comprehensibility, and from type theorists on their correctness.
Thanks for the pointer. Hm, on the github-page it says
The file you want to compile is
I’d rather not compile any of your files, but just open a pdf.
Not being the greatest tex expert, my compiler is struggling at line 4 (\newif\ifcref\creftrue), and I don’t know what to do.
Also, unless one also grabs the bibtex file, none of the references will work (I cloned the repo in my Desktop installation of GitHub and ran ’build’ in Sublime Text, which took some time but still gave lots of warnings. I didn’t bother trying to get the refs)
here’s a pdf for the impatient :) (edit: added refs)
p. 11 in “exhibit the most behavior most characteristic of type theories” probably one superfluous “most”
David C, I can’t help you unless you can be more specific than “struggling”. My bib file is in this repo. Sorry everyone, this is a working draft and I don’t have the time to distribute pretty copies myself. (-:
So with all this repository technology, there is no way that whenever you recompile your pdf, the output gets uploaded to the git-hub page?
I can see Matt’s (#12), sot that’s fine.
The whole point of source control software is to control the source, not the compiled version. Is it really so hard to git clone?
FYI, here is a compiled current version that I’m going to point the students at tomorrow.
1 to 18 of 18