Not signed in (Sign In)

Start a new discussion

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

Discussion Tag Cloud

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.
    • CommentAuthormaxsnew
    • CommentTimeJan 11th 2018

    I want to record a certain lemma on the nlab that is rarely made explicit (slight variation here: https://arxiv.org/abs/1112.0094).

    The theorem is that if you have a profunctor RR from CC to DD and it is representable as a functor F:CDF : C \to D then the action of FF on morphisms is uniquely determined by RR and the representation isomorphism.

    This explains the initially strange feature of type theoretic connectives, which have semantics as functors but we never actually define their action on morphisms because we can derive the action from the introduction and elimination rules.

    My question is should this get a page on the nlab, called I guess “Representability determines Functoriality” or something like that? Or should I try to find some existing page?

    And a meta-question is should I err on the side of just making a page with whatever name I feel like or come to discuss the name here on the nforum? Is it easy to change names of pages after the fact?

    • CommentRowNumber2.
    • CommentAuthorUrs
    • CommentTimeJan 11th 2018

    It is easy to change the name of a page: There is a check box below the edit pane. Click on it and enter a new name in the dialogue box. The old name will automatically be made a redirect. So you don’t have to worry much about naming.

    Also, it is established practice here to create a page that is named not after a definition, but after a fact. (That’s living propositions-as-types, I suppose.)

    So I would say: Feel free to go ahead!

    • CommentRowNumber3.
    • CommentAuthorUrs
    • CommentTimeJan 11th 2018
    • (edited Jan 11th 2018)

    Ah, just one thing: We have the convention not to have capitals in entry names, unless they are given names (e.g. book titles).

    • CommentRowNumber4.
    • CommentAuthormaxsnew
    • CommentTimeJan 12th 2018

    Thanks, Urs. I made the page representability determines functoriality with just the formula for now and will probably add more detail soon.

    • CommentRowNumber5.
    • CommentAuthorUrs
    • CommentTimeJan 12th 2018

    Thanks. I have cross-linked with the entry profunctor (briefly here), so that the new entry may be found.

    You will probably add cross-links from/to the relevant type theory entries that you have in mind.

    • CommentRowNumber6.
    • CommentAuthormaxsnew
    • CommentTimeJan 24th 2018

    Ok I’ve added another lemma that says you can present a functor with a representation from the data given in type theory and functoriality and naturality follow from the definition of substitution and β,η\beta,\eta. I don’t know of any references for that theorem exactly, but it’s probably somewhere/folklore.

    • CommentRowNumber7.
    • CommentAuthorMike Shulman
    • CommentTimeFeb 18th 2018

    I changed ε c:R(c,F 0c)\epsilon_c : R(c,F_0c) to ε c:R(F 0c,c)\epsilon_c : R(F_0c,c), since it seems from the other notation that the convention is R:D op×CSetR : D^{op} \times C\to Set.

    • CommentRowNumber8.
    • CommentAuthorMike Shulman
    • CommentTimeFeb 18th 2018

    Also, doesn’t “left-naturality of ι\iota” follow from “isomorphism”, since R(,id)(ε)R(-,id)(\epsilon) is always natural and a pointwise inverse of a natural transformation is automatically natural?

    • CommentRowNumber9.
    • CommentAuthorDavid_Corfield
    • CommentTimeFeb 22nd 2018

    Section 5 doesn’t make sense as stated, does it?

    In equation (1) the first RR should be R ×R_{\times}, but then the further RRs don’t make sense, and presumably should be Hom C(A,B)Hom_C(A, B), etc.

    The choice of CC for category and object is not ideal.

    Given the choice of BB and CC in the product, wouldn’t it be better to have these index the projections?

    • CommentRowNumber10.
    • CommentAuthormaxsnew
    • CommentTimeFeb 22nd 2018

    Thanks, I’ve changed the notation in section 5

    • CommentRowNumber11.
    • CommentAuthormaxsnew
    • CommentTimeFeb 22nd 2018

    Also re: the other thread, I’ve made the “main theorem” of the page more explicit.

    • CommentRowNumber12.
    • CommentAuthorDavid_Corfield
    • CommentTimeFeb 22nd 2018

    Thanks!

Add your comments
  • Please log in or leave your comment as a "guest post". If commenting as a "guest", please include your name in the message as a courtesy. Note: only certain categories allow guest posts.
  • To produce a hyperlink to an nLab entry, simply put double square brackets around its name, e.g. [[category]]. To use (La)TeX mathematics in your post, make sure Markdown+Itex is selected below and put your mathematics between dollar signs as usual. Only a subset of the usual TeX math commands are accepted: see here for a list.

  • (Help)