double categories

Stream: Is there code for X?

[Dorette Pronk]

One of my students will be working this summer on studying fibrations of double categories using Lean and developing the code needed. He will start by creating the definition etc in Lean. However, we were wondering whether there are preferences in the community for the way we do this. The first question is whether we implement them as internal categories in Cat (I think that internal categories still need to be introduced as well) or as a new type of category that has two types of arrows and double cells, etc. Of course one can easily be turned into the other. The other question is whether we can just introduce strict double categories and leave the weaker versions to be developed in the future. (For our current project we only need strict ones.) I have noticed that for 2-categories and bicategories it seems that the community has taken the approach that bicategories are defined and 2-categories are a special kind of bicategories (please correct me if I have missed something). There are a couple of ways of making double categories weaker and providing all the code to do this is significantly more work (plus that my student is just learning about double categories and I would rather have him become familiar with the strict version before he needs to take care of all the additional structure cells and coherence).

[Reid Barton]

I think you're right that we don't have any kind of internal categories yet, not even ordinary categories as category internal to Set/Type. (Maybe someone like @Adam Topaz or @Bhavik Mehta can confirm that?)

[Reid Barton]

We only have categories defined in the dependently typed/GAT-style. The issue with bicategories vs strict 2-categories is then that if you try to give a GAT-style definition of a strict 2-category, then I think some of the equations only type check if your type theory is extensional, which Lean is not. So, you effectively have to insert some "associators" anyways in the form of transport (eq.rec) across equalities $(fg)h = f(gh)$. At that point, it is our experience that it is easier to just treat these associators as extra structure in the first place.

[Reid Barton]

I guess double categories will encounter the same issue. That is, if part of the data of a double category is

(sqs : \Pi (A B C D : Ob) (f : HHom A B) (g : HHom C D) (h : VHom A C) (k : VHom B D), Type)
   -- type of squares with a prescribed boundary

then the associativity axiom for horizontal composition of squares (say) will lie "over" the associativity axiom for composition of horizontal morphisms.

[Reid Barton]

Likewise, I assume the conditions to be a fibration involve some on-the-nose equalities of cells that will be awkward to state in this style. I think the internal category style definition is better suited for this purpose (and they should be internal categories in (internal categories in Set), not internal categories in docs#category_theory.Cat).

[Reid Barton]

However, this is currently unexplored territory, as mentioned earlier