Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
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?
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!
Ah, just one thing: We have the convention not to have capitals in entry names, unless they are given names (e.g. book titles).
Thanks, Urs. I made the page representability determines functoriality with just the formula for now and will probably add more detail soon.
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.
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.
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$.
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?
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?
Thanks, I’ve changed the notation in section 5
Also re: the other thread, I’ve made the “main theorem” of the page more explicit.
Thanks!
1 to 12 of 12