from a Cat-enriched category to a strict bicategory

Stream: mathlib4

[Emily Riehl]

Today the #**Infinity-Cosmos> project proved that a Cat-enriched category defines a strict bicategory; see #25287.

@Mario Carneiro was able to golf the proof significantly by introducing an explicit definition that we're calling hcomp for the horizontal composition of 2-cells. I don't believe this is defined explicitly for bicategories and I'm curious why not. Maybe @Yuma Mizuno or others could comment?

I know that horizontal composition can be recovered (in two ways) from vertical composition of whiskering, and there is some ambiguity over which of two definitions to prioritize. So perhaps that is the reason that is is missing. When the starting point is a Cat-enriched category this definition is more canonical, which is perhaps why it appears more centrally here. @Mario Carneiro can say more about the simplifications it led to in the construction of the bicategory structure.

[Mario Carneiro]

can it maybe be extra data? I did find it easier to work with then either of the whiskerings

[Robert Maxton]

I recall running across a reasoning for this... somewhere...
Ah.

Yuma Mizuno said:

I would like to make a comment that are not intended to interfere with the current PR.

The proofs in the PR #14402 contain several rewriting of the form (𝟙 _ ⊗ f) ≫ (g ⊗ 𝟙 _) = (g ⊗ 𝟙 _) ≫ (𝟙 _ ⊗ f). In fact, these are equal to tensor_hom, g ⊗ f.

In my experience, tensor_hom seems to be incompatible with simp. I think this can be improved by introducing whisker_right and whisker_left as the primitive objects in the definition of the monoidal category rather than tensor_hom, as I did in the definition of bicategory, which uses whisker_right and whisker_left instead of the horizontal compositions. I would like to do this kind of a refactoring if I can find the time.

[Yuma Mizuno]

Emily Riehl said:

@Mario Carneiro was able to golf the proof significantly by introducing an explicit definition that we're calling hcomp for the horizontal composition of 2-cells. I don't believe this is defined explicitly for bicategories and I'm curious why not. Maybe @Yuma Mizuno or others could comment?

The constructor using hcomp is currently missing in mathlib, but the reason is simply that it hasn't been needed until now. I chose to use whiskering in the definition rather than hcomp because it can be interpreted as a more primitive building block, and therefore I thought it would work well with simp.

[Emily Riehl]

@Yuma Mizuno while you're here, could you explain whether a horizontal composition α : f --> g followed by β : h --> k has a simp normal form and if so what is it? More generally, if I have an arbitrary pasted composite in a bicategory, does it have a unique simp normal form? Essentially i'd like to better understand that section of the bicategories file, which I believe you wrote.

[Yuma Mizuno]

There is no simp normal form at the moment, which is an intentional design choice.

I think simp is generally insufficient to deal with arbitrary pasted compositions, and we need a specific tactic for that.

[Yuma Mizuno]

Actually the horizontal composition has not yet been defined, so for now we can only write a formula with explicit ordered 2-morphisms.

[Yuma Mizuno]

I found that "no simp normal form" might be confusing.

To be explicit, both f ◁ β ≫ α ▷ k and α ▷ h ≫ g ◁ β are simp normal forms.