Bicategory terminology

[maxsnew]

Categories.Bicategory.agda defines the following as "horizontal composition"

  -- horizontal composition
  _∘ₕ_ : {A B C : Obj} → B ⇒₁ C → A ⇒₁ B → A ⇒₁ C
  _∘ₕ_ = _⊚₀_

This terminology is a bit strange to me. This is the composition of the 1-cells, whereas I've always heard "horizontal composition" to refer to the "parallel" composition of 2-cells, as here, which is in the library of course:

  _⊚₁_ : {A B C : Obj} {f h : B ⇒₁ C} {g i : A ⇒₁ B} → f ⇒₂ h → g ⇒₂ i → f ⊚₀ g ⇒₂ h ⊚₀ i
  α ⊚₁ β = Functor.F₁ ⊚ (α , β)

I think the traditional terminology makes sense because vertical/horizontal are both constructions on 2-cells. I suggest we rename _∘ₕ_ to be an alias for _⊚₁_, and maybe we can give _∘₁_ as the alias for 1-cell composition instead.

[JacquesCarette]

git blame points to @HuStmpHrrr . I'm surprised that @sstucki didn't mention anything, since he's played around with Bicategory more than anyone else.

[HuStmpHrrr]

yes, this is awkward. I agree with this change.

[maxsnew]

Ok so this is a somewhat big breaking change are we agreed on it before I do it?

[JacquesCarette]

Since the main author agrees and I, as principal maintainer, am fine with this change, I think that's a "yes".