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.
1 to 8 of 8
In my opinion, the question of equipping a category of algebraic Kan complexes, or something similar, with a closed monoidal structure is a very important and interesting one.
I don’t know whether you have seen it, but I made a few remarks on this in a cubical setting here. In particular, I do think that the category of cubical algebraic Kan complexes should be able to be equipped with a closed monoidal structure. However, if one experiments a little, it is clear that it is a subtle and interesting matter, closely related to pinning down how we wish to think of algebraic Kan complexes as -groupoids. This underlies the point that the category of algebraic Kan complexes, where morphisms preserve the chosen fillers, is very different from the ordinary category of cubical sets.
The monoidal structure that I think should exist on cubical algebraic Kan complexes would not be cartesian, though, but I would not expect it to be: the ’correct’ monoidal structure on higher categories seems to me to be Gray-like, not cartesian.
It may be that the category of algebraic Kan complexes itself may not quite be able to be equipped with the closed monoidal structure that I have in mind: one might need to tweak it a little. But the morphisms will still preserve fillers.
Regarding your suggestion for a category of ’functional Kan complexes’, one could of course consider it, but I would strongly disagree that the objects of this category can be thought of as algebraic -groupoids. It is precisely the fact that morphisms preserve the chosen fillers that is significant about the category of algebraic Kan complexes, and which differentiates its behaviour from the usual category of simplicial/cubical sets. This fact is I think not emphasised enough about algebraic Kan complexes: the fact that we choose fillers on the objects doesn’t really change anything from a categorical point of view. Indeed, as of course you will know, the latter is really the only way that one can make the definition of a Kan complex in a strong constructive foundations (it is the question of the meaning of the existential quantifier).
I also think that one should be able to show closure of the non-cartesian monoidal structure on cubical ’functional Kan complexes’ in a constructive way: at least, I think it possible that the most one will need is to be able to argue by cases on finite sets of natural numbers. Definitely the axiom of choice should not be necessary.
I didn’t quite follow your remark about fillers being sent to fillers by naturality: could you elaborate upon it?
Thank you, I see what you mean now!
(replying to this in order not to have to start a dicussion on account of such a small change)
Edited both filler and Kan complex; links added in the latter, building on a contribution of Tim Porter in the former.
[edit: After working through my backlog, I see now that others here have expressed the same as below before. Peter, please wait for a while with creating many more entries, as it’s going a little against the grain of the way we usually proceed. ]
Peter,
we usually do not create a separate page for each synonym. It seems more efficient to have all the information in one place and instead have the synomyms be redirects to that page.
If in a given entry XYZ you add line of the form
[[!redirects ABC]]
then the URL
https://ncatlab.org/nlab/show/ABC
will take the user to the same place as
https://ncatlab.org/nlab/show/XYZ
I suggest filler and diagonal fill-in should all redirect to lift. At the very least “diagonal fill-in” should be but a redirect to “filler”.
Merged diagonal fill-in into filler, according to the HowTo and the comments, which seems an improvement. Merging into lift would require more care. If it is strongly preferred to do so, too, will do this sometime in the future.
I added some organizational structure to filler, and a few more words and links.
1 to 8 of 8