Not signed in (Sign In)

Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

  • Sign in using OpenID

Site Tag Cloud

2-category 2-category-theory abelian-categories adjoint algebra algebraic algebraic-geometry algebraic-topology analysis analytic-geometry arithmetic arithmetic-geometry book bundles calculus categorical categories category category-theory chern-weil-theory cohesion cohesive-homotopy-type-theory cohomology colimits combinatorics complex complex-geometry computable-mathematics computer-science constructive cosmology deformation-theory descent diagrams differential differential-cohomology differential-equations differential-geometry digraphs duality elliptic-cohomology enriched fibration foundation foundations functional-analysis functor gauge-theory gebra geometric-quantization geometry graph graphs gravity grothendieck group group-theory harmonic-analysis higher higher-algebra higher-category-theory higher-differential-geometry higher-geometry higher-lie-theory higher-topos-theory homological homological-algebra homotopy homotopy-theory homotopy-type-theory index-theory integration integration-theory internal-categories k-theory lie-theory limits linear linear-algebra locale localization logic mathematics measure measure-theory modal modal-logic model model-category-theory monad monads monoidal monoidal-category-theory morphism motives motivic-cohomology nlab noncommutative noncommutative-geometry number-theory of operads operator operator-algebra order-theory pages pasting philosophy physics pro-object probability probability-theory quantization quantum quantum-field quantum-field-theory quantum-mechanics quantum-physics quantum-theory question representation representation-theory riemannian-geometry scheme schemes set set-theory sheaf simplicial space spin-geometry stable-homotopy-theory stack string string-theory superalgebra supergeometry svg symplectic-geometry synthetic-differential-geometry terminology theory topology topos topos-theory tqft type type-theory universal variational-calculus

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).
    • CommentRowNumber1.
    • CommentAuthorMike Shulman
    • CommentTimeJun 10th 2016

    Can anyone suggest a naturally-occurring monoidal category whose terminal object 11 is not the unit of the monoidal structure and where also 1111\otimes 1\ncong 1?

    • CommentRowNumber2.
    • CommentAuthorOscar_Cunningham
    • CommentTimeJun 10th 2016
    • (edited Jun 11th 2016)

    What about Set\mathbf{Set}, taking \otimes to be the coproduct?

    • CommentRowNumber3.
    • CommentAuthorMike Shulman
    • CommentTimeJun 11th 2016

    Okay, yeah, of course, I simplified too much. How about a closed monoidal category with these properties?

    • CommentRowNumber4.
    • CommentAuthorTodd_Trimble
    • CommentTimeJun 11th 2016
    • (edited Jun 11th 2016)

    A cheap response is to tweak Oscar’s example to (Fin,=+)(Fin, \otimes = +), and pass to Set Fin opSet^{Fin^{op}} via Day convolution.

    Why do you want to know? :-)

    • CommentRowNumber5.
    • CommentAuthorTodd_Trimble
    • CommentTimeJun 11th 2016

    Here might be a “more natural” example: do the same as in the last comment, but with Δ\Delta in place of FinFin, with its usual tensor product (corresponding to simplicial join). I.e., pass to simplicial sets with the induced tensor product.

    • CommentRowNumber6.
    • CommentAuthorMike Shulman
    • CommentTimeJun 11th 2016

    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 ,1,+,0,×,,\otimes,1,+,0,\times,\top,\multimap) that presents a free closed monoidal category with products and coproducts. And I noticed that the term for the unique inhabitant of \top (the additive truth, i.e. the terminal object) can’t be just “tttt” the way it is in cartesian type theory, but has to take all the variables from the context as arguments. Otherwise a term like x:tt,tt:x:\top \vdash \langle tt,tt\rangle : \top\otimes \top is ambiguous; we ought to write either tt(x),tt\langle \tt(x),tt\rangle or tt,tt(x)\langle \tt,tt(x)\rangle. 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.)

    • CommentRowNumber7.
    • CommentAuthorUrs
    • CommentTimeJun 11th 2016

    Are you typing up notes to go with this? I’d enjoy seeing them.

    • CommentRowNumber8.
    • CommentAuthorMike Shulman
    • CommentTimeJun 13th 2016

    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.

    • CommentRowNumber9.
    • CommentAuthorUrs
    • CommentTimeJun 13th 2016

    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.

    • CommentRowNumber10.
    • CommentAuthorDavid_Corfield
    • CommentTimeJun 13th 2016

    Not being the greatest tex expert, my compiler is struggling at line 4 (\newif\ifcref\creftrue), and I don’t know what to do.

    • CommentRowNumber11.
    • CommentAuthorDavidRoberts
    • CommentTimeJun 13th 2016

    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)

    • CommentRowNumber12.
    • CommentAuthorMatt Earnshaw
    • CommentTimeJun 13th 2016
    • (edited Jun 13th 2016)

    here’s a pdf for the impatient :) (edit: added refs)

    • CommentRowNumber13.
    • CommentAuthorUrs
    • CommentTimeJun 13th 2016

    p. 11 in “exhibit the most behavior most characteristic of type theories” probably one superfluous “most”

    • CommentRowNumber14.
    • CommentAuthorMike Shulman
    • CommentTimeJun 13th 2016

    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. (-:

    • CommentRowNumber15.
    • CommentAuthorUrs
    • CommentTimeJun 14th 2016
    • (edited Jun 14th 2016)

    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?

    • CommentRowNumber16.
    • CommentAuthorDavid_Corfield
    • CommentTimeJun 14th 2016

    I can see Matt’s (#12), sot that’s fine.

    • CommentRowNumber17.
    • CommentAuthorMike Shulman
    • CommentTimeJun 14th 2016

    The whole point of source control software is to control the source, not the compiled version. Is it really so hard to git clone?

    • CommentRowNumber18.
    • CommentAuthorMike Shulman
    • CommentTimeJul 10th 2016

    FYI, here is a compiled current version that I’m going to point the students at tomorrow.