-
Notifications
You must be signed in to change notification settings - Fork 197
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Defined Bicategory #2215
base: master
Are you sure you want to change the base?
Defined Bicategory #2215
Conversation
I think that merging the definition of a bicategory and a monoidal category wouldn't be the right direction. It's best to treat monoidal categories as 1-categories with extra structure rather than a special case of bicategories. There is another direction we could think of unifying however, and that is with We will need to have a deeper think about how to structure the intermediate parts so we can share more, but for now I would suggest making some intermediate structures to parallel the buildup of TwoOneCat and we can think about merging those with the normal category buildup later. Regarding notations, we will have some confusion with Also it would be nice to show that we have a bicategory of categories, functors and natural transformations as an example, since this is the example we wish to generalise to arguments elsewhere. For now this can be in the same file. My only other comment would be to avoid having large amounts of arguments as we currently do since it will negatively impact performance, some bundling with the intermediate structures I described above will help with this. Just so we are on the same page, is there a specific project that you wish to formalise this for? Knowing that can help us lay the theory out a bit better. |
I'll read the
I'm writing a paper right now where I need some basic theory of (strict) 2-fibrations of 2-categories. In particular there should be an analogue of the 1-categorical theorem that if the fibers of a Grothendieck fibration have limits and reindexing functors preserve those limits, then the total category of the fibration is complete; one should be able to get a similar theorem for 2-limits. Something similar should be true for bicategories and fibrations of bicategories. It might get tedious but I was thinking it might be interesting to try and write some rewriting tactics using this problem as motivation. It might be best to first continue the existing theory of displayed categories to establish the 1-categorical limit lifting theorem and then move on to the higher-categorical analogue. |
Sounds interesting! |
@Alizter Hi, Ali. I have looked at the code for |
@Alizter Follow-up question: in |
@patrick-nicodemus For 1-cats we have 1-cells and 2-cells. The 2-cells play the role of "setoid equality". For a 2-cat I would expect us to have 1-cells, 2-cells and 3-cells playing the role of "setoid equality". The associatiator would be an invertible 2-cell, i.e. a (natural) equivalence. When we have a bicategory and the 2-cells are invertible, we would get a TwoOneCat because equivalences would form a 1-groupoid. There is probably a "core" functor taking (2,2)-cats to (2,1)-cats. Regarding naturality, you are welcome to either do them together or separately. In either case, it is some work to go to the other. I would probably aim for together and derive separate versions as a lemma or smart constructor. See |
I'm not sure if @Alizter understood your question. Are you talking about these two lines: is1cat_hom : forall (a b : A), Is1Cat (a $-> b) ;
is1gpd_hom : forall (a b : A), Is1Gpd (a $-> b) ; ? If so, I believe that the 1-groupoid structure on |
@jdchristensen Yep, that's it. Well, close to that - there are also the 2-cells which are already present in the assumption Thanks for helping me figure that out, I wasn't understanding how the typeclass sharing was working there but I see now that |
Oh, right, there's |
c96c140
to
bf75e79
Compare
bf75e79
to
2a843f2
Compare
@jdchristensen I have cleaned up the style issues and I think this is ready for more serious review and discussion. |
Thanks! I'm going to be travelling for a bit, so I won't be able to look at it closely for a while. But @Alizter knows more about the wild categories library anyways, so hopefully he can provide some feedback. |
I will get round to reviewing this properly soon. It will take some time to look through thoroughly. |
f1c0915
to
dd2ca5c
Compare
I think having (2,1)-cats and bicats share this much makes implementing this much harder than it needs to be. I agree that there is redundancy between the two definitions, but we should probably leave reducing that till later. I would prefer if we could just write down a definition of bicat in a separate file and not touch much else. That way we can review and develop this idea further and perhaps introduce sharing. This should revert much of the changes due to tweaks with TwoOneCat. The main issue with sharing is that homs in a (2,1)-cat are directly 1-cats, but thats only true about the (2-)core of homs in a bicat. There is probably a better way to organise this, but for now lets lay everything out clearly. It would also be better if you introduce any new notions like |
I don't understand this comment. My proposed definition of a bicategory says:
|
I think that the proposed definition is of sufficiently general utility (an obviously symmetric way of talking about of invertible morphisms) that I would prefer to put it somewhere where it can be imported without also importing too many unrelated dependencies. What do you think of me keeping it where it is and adding a clear comment which explains the motivation (it allows talking about invertible morphisms that plays well with passing from C to C^op) and refers the reader to the bicategory file? |
The issue I have with Regarding your other comment, I seem to be confused. I think I misunderstood something. I'll come back to this and clear up my confusion. |
I also think the name of a "truncated bicategory" has to be chosen well. The term "truncated" is somewhat overloaded in homotopy theory, I feel: what this page terms the n-skeleton and the n-coskeleton (https://ncatlab.org/nlab/show/simplicial+skeleton) both seem to be casually referred to as "n-truncation" and I feel it's often ambiguous what is meant. Perhaps |
Note that existing My intent with this design is to stratify the structure of a bicategory into two levels, the first containing all (0,1,2)-cells and the second containing all appropriate 3-cells. If we assume the associator 2-cell in stage A, and then assume it's an I like my stratified design because I think there are many theorems about 1-categories which should hold for |
To me the main sharing issue is that a "truncated bicategory" has hom-sets such that |
Specifically, we've got the following. Not sure if it would handle what
|
@jdchristensen It's pretty close. I want to organize things as:
If we could introduce a more unbundled variant of (In the theory of 1-cats, the right-to-left associator 2-cell is not necessary because we have already assumed that all 2-cells are invertible.) |
Look, we already have something which is almost exactly what I want here in WildCat/Core.v :
We want to say that the pre-existing "inverse"
|
I will play around with it more this weekend with some examples I had in mind. There are a few other tweaks I would like to try out and I'll suggest them if they work out. Thanks for starting this, I think it will be very useful. |
This defines a bicategory, mimicking the definition in Monoidal.v.
There is no sharing between the bicategory definition and the monoidal category definition. If you think this could be refactored to remove redundancy between files, let me know.
In the spirit of the typeclass-based approach to the Wildcat library, where you only assume what is necessary at each step, it would be interesting to introduce the concept of a "2-truncated bicategory" which is a weakening of a 1-category such that Hom(a, b) is a 0-category rather than a 0-groupoid, and define a 1-category to be a 2-truncated bicategory such that all Hom-0-cats are 0-groupoids. It seems likely that a good share of category theory can be carried out for these 2-truncated bicategories, so this would eliminate some duplication in theorems about bicategories and 1-categories. However this is a more substantial project.