Skip to content
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

Open
wants to merge 4 commits into
base: master
Choose a base branch
from

Conversation

patrick-nicodemus
Copy link
Contributor

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.

@Alizter
Copy link
Collaborator

Alizter commented Feb 17, 2025

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 TwoOneCategory.v. In order to do this however, we need to separate out the invertability of the second level in Is1Cat so that TwoOneCat becomes a special case of bicategory where the 2-cells are invertible.

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 a $-> b being a 1-cell or a 2-cell, so I would suggest introducing a $=> b like we do for NatTrans to denote specifically the 2-cell. i.e. Hom (A:=Hom _ _).

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.

@patrick-nicodemus
Copy link
Contributor Author

I'll read the TwoOneCategory.v file, I'm not familiar with that.
I'm happy to switch to more bundled structures.
I agree that the bicategory of categories, functors and natural transformations is a good example.
Another example might be the bicategory of types and "spans" R : A -> B -> Type.

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

@jdchristensen
Copy link
Collaborator

Sounds interesting!

@patrick-nicodemus
Copy link
Contributor Author

@Alizter Hi, Ali. I have looked at the code for TwoOneCat. Do you think it is necessary to have two distinct relations on the 1-cells of a (2,1)-cat: both 2-cells between them and setoid equality; and composition is bifunctorial with respect to both setoid equality and 2-cells? I suspect one could probably get away with only the 2-cells.

@patrick-nicodemus
Copy link
Contributor Author

@Alizter Follow-up question: in TwoOneCat the associator is defined to be natural in each variable separately while the others are held constant; in Monoidal the associator is defined to be natural between all variables at once as a functor on the product category. What do you think should be the convention?

@Alizter
Copy link
Collaborator

Alizter commented Feb 18, 2025

@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 Bifunctor.v for a similar situation.

@jdchristensen
Copy link
Collaborator

I have looked at the code for TwoOneCat. Do you think it is necessary to have two distinct relations on the 1-cells of a (2,1)-cat: both 2-cells between them and setoid equality;

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 a $-> b uses the same morphisms as the 1-category structure, so there aren't two separate types of 2-cells. The first line says that there are 2-cells (with some properties) and the second line says that they are invertible.

@patrick-nicodemus
Copy link
Contributor Author

patrick-nicodemus commented Feb 18, 2025

@jdchristensen Yep, that's it. Well, close to that - there are also the 2-cells which are already present in the assumption Is1Cat A before the code you posted, because since A Is1Cat its hom-sets are already equipped with setoid equality.

Thanks for helping me figure that out, I wasn't understanding how the typeclass sharing was working there but I see now that Is1Cat in is1cat_hom depends on/re-uses the Is01Cat typeclass for a $->b which is assumed in the first line Is1Cat A.

@jdchristensen
Copy link
Collaborator

Yep, that's it. Well, close to that [...]

Oh, right, there's Is1Cat A, and Is3Graph A, so it's not obvious what's being reused and what's new. But I'm pretty sure it's true that there is just one kind of 2-cell. Is1Cat A isn't preceded by an exclamation mark, so it implies its dependencies, which include Is2Graph A, i.e. that there are 2-cells. But Is3Graph A does have an exclamation mark, it it reuses those. For the two I quoted above, they don't introduce any cells of their own (and since they aren't introduced using backtick notation, there is no risk that their dependencies get added as additional data). So there should just be one set of 2-cells.

@patrick-nicodemus patrick-nicodemus marked this pull request as ready for review February 21, 2025 08:40
@patrick-nicodemus patrick-nicodemus force-pushed the bicategory branch 3 times, most recently from c96c140 to bf75e79 Compare February 25, 2025 15:50
@patrick-nicodemus
Copy link
Contributor Author

@jdchristensen I have cleaned up the style issues and I think this is ready for more serious review and discussion.

@patrick-nicodemus patrick-nicodemus mentioned this pull request Feb 25, 2025
@jdchristensen
Copy link
Collaborator

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

@Alizter
Copy link
Collaborator

Alizter commented Feb 25, 2025

I will get round to reviewing this properly soon. It will take some time to look through thoroughly.

@Alizter Alizter self-requested a review February 25, 2025 19:29
@Alizter
Copy link
Collaborator

Alizter commented Mar 13, 2025

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 InverseOf directly in the bicat file so we can better appreciate its motivation.

@patrick-nicodemus
Copy link
Contributor Author

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.

I don't understand this comment. My proposed definition of a bicategory says:

 Class IsBicategory (A : Type) `{Is01Cat A} `{!Is2Graph A} `{!Is3Graph A} := {
  is_truncated_bicat:: IsTruncatedBicat A;
  is1cat_2cells:: forall (a b : A), Is1Cat (Hom a b);

@patrick-nicodemus
Copy link
Contributor Author

It would also be better if you introduce any new notions like InverseOf directly in the bicat file so we can better appreciate its motivation.

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?

@Alizter
Copy link
Collaborator

Alizter commented Mar 13, 2025

The issue I have with InverseOf is that we already have a way of taking about invertible morphisms, that's the point of WildCat/Equiv.v.

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.

@patrick-nicodemus
Copy link
Contributor Author

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 Is1Bicategory would be a good name, if the convention chosen is that for a natural number n and a term X, the class IsnX refers to a wild category structure which contains all cells up to the (n+1)-th layer.

@patrick-nicodemus
Copy link
Contributor Author

patrick-nicodemus commented Mar 13, 2025

@Alizter

The issue I have with InverseOf is that we already have a way of taking about invertible morphisms, that's the point of WildCat/Equiv.v.

Note that existing TwoOneCat.v file does not use Equiv.v at all, it assumes that the type of 2-cells f $=> g is a 1-gpd for 1-cells f,g. Thus the associator is not an Equiv, it is just a 2-cell subject to some 3-cells. If you want to take this PR as an opportunity to rethink this design, fine by me.

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 Equiv in stage B, then we are missing the inverse of the associator at stage A, which defeats the purpose of dividing it into two stages, because a bicategory with only a left-to-right associator is not a very interesting mathematical structure.

I like my stratified design because I think there are many theorems about 1-categories which should hold for TruncatedBicategories with little to no change. If it is feasible to refactor Equiv.v in such a way that one can speak of CatIsEquiv f g over a pair f, g of given morphisms (i.e. somehow the given equivalence is an adjointification of the pair f, g) then we could incorporate both of these perspectives.

@patrick-nicodemus
Copy link
Contributor Author

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

To me the main sharing issue is that a "truncated bicategory" has hom-sets such that Hom a b is a 01-cat for all a,b, and a 1Cat is precisely a truncated bicategory such that these Hom-01-cats are 0-gpds. So if there is refactoring to be done, ideally it would be to make Is1Cat rely on IsTruncatedBicat, but of course this would be a very substantial refactoring, so the emphasis on "ideal" is heavy.

@jdchristensen
Copy link
Collaborator

The issue I have with InverseOf is that we already have a way of taking about invertible morphisms, that's the point of WildCat/Equiv.v.

Specifically, we've got the following. Not sure if it would handle what InverseOf was created for.

Class Cat_IsBiInv {A} `{Is1Cat A} {x y : A} (f : x $-> y) := {
  cat_equiv_inv : y $-> x;
  cat_eisretr : f $o cat_equiv_inv $== Id y;
  cat_equiv_inv' : y $-> x;
  cat_eissect' : cat_equiv_inv' $o f $== Id x;
}.

Record Cat_BiInv A `{Is1Cat A} (x y : A) := {
  cat_equiv_fun :> x $-> y;
  cat_equiv_isequiv : Cat_IsBiInv cat_equiv_fun;
}.

@patrick-nicodemus
Copy link
Contributor Author

patrick-nicodemus commented Mar 13, 2025

@jdchristensen It's pretty close. I want to organize things as:

  • in stage A, we say "there is a left-to-right associator 2-cell, and a right-to-left associator 2-cell"
  • in stage B, we say "there are 3-cells making these each others' two-sided inverse"

If we could introduce a more unbundled variant of Cat_IsBiInv which is parameterized by both f and cat_equiv_inv then this would fit what I am looking for.

(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.)

@patrick-nicodemus
Copy link
Contributor Author

patrick-nicodemus commented Mar 13, 2025

Look, we already have something which is almost exactly what I want here in WildCat/Core.v :

Class Is1Gpd (A : Type) `{Is1Cat A, !Is0Gpd A} :=
{
  gpd_issect : forall {a b : A} (f : a $-> b), f^$ $o f $== Id a ;
  gpd_isretr : forall {a b : A} (f : a $-> b), f $o f^$ $== Id b ;
}.

We want to say that the pre-existing "inverse" f^$ (already assumed by Is0Gpd) is a two-sided inverse to f, it would be somehow inappropriate to say that a 1Gpd is just a 1Cat where every 1-cell is Cat_IsBiInv, because then it would not extend 0Gpd at all. So in a sense AreInverse is not new code, it is just abstracting out something which already appears in the library. We would rewrite Is1Gpd as

Class Is1Gpd (A : Type) `{Is1cat A, !Is0Gpd A} := forall {a b : A}, AreInverse f f^$

@Alizter
Copy link
Collaborator

Alizter commented Mar 13, 2025

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.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants