Not signed in

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

• Forgot your password?
• Apply for membership

1. • CommentRowNumber1.
   • CommentAuthormaxsnew
   • CommentTimeJan 11th 2018
   • PermaLink
   Author: maxsnew
   Format: MarkdownItexI 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 $R$ from $C$ to $D$ and it is representable as a functor $F : C \to D$ then the action of $F$ on morphisms is uniquely determined by $R$ 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?

   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 $R$ from $C$ to $D$ and it is representable as a functor $F : C \to D$ then the action of $F$ on morphisms is uniquely determined by $R$ 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?

2. • CommentRowNumber2.
   • CommentAuthorUrs
   • CommentTimeJan 11th 2018
   • PermaLink
   Author: Urs
   Format: MarkdownItexIt 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!

   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!

3. • CommentRowNumber3.
   • CommentAuthorUrs
   • CommentTimeJan 11th 2018
   • (edited Jan 11th 2018)
   • PermaLink
   Author: Urs
   Format: MarkdownItexAh, just one thing: We have the convention not to have capitals in entry names, unless they are given names (e.g. book titles).

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

4. • CommentRowNumber4.
   • CommentAuthormaxsnew
   • CommentTimeJan 12th 2018
   • PermaLink
   Author: maxsnew
   Format: MarkdownItexThanks, Urs. I made the page [[representability determines functoriality]] with just the formula for now and will probably add more detail soon.

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

5. • CommentRowNumber5.
   • CommentAuthorUrs
   • CommentTimeJan 12th 2018
   • PermaLink
   Author: Urs
   Format: MarkdownItexThanks. I have cross-linked with the entry _[[profunctor]]_ (briefly [here](https://ncatlab.org/nlab/show/profunctor#Properties)), 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.

   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.

6. • CommentRowNumber6.
   • CommentAuthormaxsnew
   • CommentTimeJan 24th 2018
   • PermaLink
   Author: maxsnew
   Format: MarkdownItexOk 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.

   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.

7. • CommentRowNumber7.
   • CommentAuthorMike Shulman
   • CommentTimeFeb 18th 2018
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexI changed $\epsilon_c : R(c,F_0c)$ to $\epsilon_c : R(F_0c,c)$, since it seems from the other notation that the convention is $R : D^{op} \times C\to Set$.

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

8. • CommentRowNumber8.
   • CommentAuthorMike Shulman
   • CommentTimeFeb 18th 2018
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexAlso, doesn't "left-naturality of $\iota$" follow from "isomorphism", since $R(-,id)(\epsilon)$ is always natural and a pointwise inverse of a natural transformation is automatically natural?

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

9. • CommentRowNumber9.
   • CommentAuthorDavid_Corfield
   • CommentTimeFeb 22nd 2018
   • PermaLink
   Author: David_Corfield
   Format: MarkdownItexSection 5 doesn't make sense as stated, does it? In equation (1) the first $R$ should be $R_{\times}$, but then the further $R$s don't make sense, and presumably should be $Hom_C(A, B)$, etc. The choice of $C$ for category and object is not ideal. Given the choice of $B$ and $C$ in the product, wouldn't it be better to have these index the projections?

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

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

   The choice of $C$ for category and object is not ideal.

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

10. • CommentRowNumber10.
    • CommentAuthormaxsnew
    • CommentTimeFeb 22nd 2018
    • PermaLink
    Author: maxsnew
    Format: MarkdownItexThanks, I've changed the notation in section 5

    Thanks, I’ve changed the notation in section 5

11. • CommentRowNumber11.
    • CommentAuthormaxsnew
    • CommentTimeFeb 22nd 2018
    • PermaLink
    Author: maxsnew
    Format: MarkdownItexAlso re: the other thread, I've made the "main theorem" of the page more explicit.

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

12. • CommentRowNumber12.
    • CommentAuthorDavid_Corfield
    • CommentTimeFeb 22nd 2018
    • PermaLink
    Author: David_Corfield
    Format: MarkdownItexThanks!

    Thanks!