Defined Bicategory

[patrick-nicodemus]

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]

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]

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]

Sounds interesting!

[patrick-nicodemus]

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

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

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

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]

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

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]

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

[jdchristensen]

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

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

[Alizter]

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]

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]

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]

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]

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]

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

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]

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]

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

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]

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.