## 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.