## Not signed in

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

## Discussion Tag Cloud

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

• 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 $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?

• 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 $\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$.

• CommentRowNumber8.
• CommentAuthorMike Shulman
• CommentTimeFeb 18th 2018

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?

• CommentRowNumber9.
• CommentAuthorDavid_Corfield
• CommentTimeFeb 22nd 2018

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?

• 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!