associator-free proof in bicategories

Stream: general

[Yuma Mizuno]

In branch#bicategory-simp-normal-form, I found that the rewriting involving associators and unitors can be much easier by rechoosing the simp lemmas. The new simp policy works well in general bicategories, and is especially useful in the rewriting in strict bicategories. For example, we can give the following "associator-free" proof for the composition of oplax natural transormations, which was originally proved by the cumbersome rewriting.

import category_theory.bicategory.strict
import category_theory.bicategory.natural_transformation
namespace category_theory
open_locale bicategory open bicategory
universes w₁ w₂ v₁ v₂ u₁ u₂
variables {B : Type u₁} [bicategory.{w₁ v₁} B]
variables {C : Type u₂} [bicategory.{w₂ v₂} C] [strict C]
variables {F G H : oplax_functor B C}
namespace oplax_nat_trans
namespace strict

-- We need strict version of simp lemmas if associators or unitors appear in the LHS.
@[simp, reassoc]
lemma whisker_right_naturality_comp (η : oplax_nat_trans F G)
  {a b c : B} {a' : C} (f : a ⟶ b) (g : b ⟶ c) (h : G.obj c ⟶ a') :
  η.naturality (f ≫ g) ▷ h ≫ eq_to_hom (by simp) ≫ η.app a ◁ G.map_comp f g ▷ h =
    F.map_comp f g ▷ η.app c ▷ h ≫ eq_to_hom (by simp) ≫
      F.map f ◁ η.naturality g ▷ h ≫ eq_to_hom (by simp) ≫
        η.naturality f ▷ G.map g ▷ h ≫ eq_to_hom (by simp) :=
by simpa using whisker_right_naturality_comp η f g h

@[simp, reassoc]
lemma whisker_right_naturality_id (η : oplax_nat_trans F G)
  {a : B} {a' : C} (f : G.obj a ⟶ a') :
  η.naturality (𝟙 a) ▷ f ≫ eq_to_hom (by simp) ≫ η.app a ◁ G.map_id a ▷ f =
    F.map_id a ▷ η.app a ▷ f ≫ eq_to_hom (by simp) :=
by simpa using whisker_right_naturality_id η f

/-- Vertical composition of oplax natural transformations. -/
@[simps]
def vcomp (η : oplax_nat_trans F G) (θ : oplax_nat_trans G H) : oplax_nat_trans F H :=
{ app := λ a, η.app a ≫ θ.app a,
  naturality := λ a b f,
    (α_ _ _ _).inv ≫ η.naturality f ▷ θ.app b ≫ (α_ _ _ _).hom ≫
      η.app a ◁ θ.naturality f ≫ (α_ _ _ _).inv,
  naturality_id' := by tidy,
  naturality_naturality' := by tidy,
  naturality_comp' := λ a b c f g, by
  { calc _ = eq_to_hom _ ≫
    F.map_comp f g ▷ _ ▷ _ ≫ eq_to_hom _ ≫
      _ ◁ η.naturality g ▷ _ ≫ eq_to_hom _ ≫
        _ ◁ θ.naturality g ≫
          η.naturality f ▷ _ ≫ eq_to_hom _ ≫
            _ ◁ θ.naturality f ▷ _ ≫ eq_to_hom _  : _
    ... =  _ : _,
    all_goals {
      -- fill underlines in `eq_to_hom _'
      solve1 { simp only [category.assoc] } <|>
      -- apply exchange law of whiskering
      { rw [whisker_exchange_assoc], simp } <|>
      -- simplify
      try { simp } } } }

end strict
end oplax_nat_trans
end category_theory

[Yuma Mizuno]

The proof for a non-strict bicategory based on the new simp policy is as follows:

import category_theory.bicategory.natural_transformation
namespace category_theory
open bicategory
open_locale bicategory
universes w₁ w₂ v₁ v₂ u₁ u₂
variables {B : Type u₁} [bicategory.{w₁ v₁} B]
variables {C : Type u₂} [bicategory.{w₂ v₂} C]
variables {F G H : oplax_functor B C}
namespace oplax_nat_trans

/-- Vertical composition of oplax natural transformations. -/
@[simps]
def vcomp' (η : oplax_nat_trans F G) (θ : oplax_nat_trans G H) : oplax_nat_trans F H :=
{ app := λ a, η.app a ≫ θ.app a,
  naturality := λ a b f,
    (α_ _ _ _).inv ≫ η.naturality f ▷ θ.app b ≫ (α_ _ _ _).hom ≫
      η.app a ◁ θ.naturality f ≫ (α_ _ _ _).inv,
  naturality_id' := by tidy,
  naturality_naturality' := by tidy,
  naturality_comp' := λ a b c f g, by
  { calc _ =  _ ≫
    F.map_comp f g ▷ η.app c ▷ θ.app c ≫ _ ≫
      F.map f ◁ η.naturality g ▷ θ.app c ≫ _ ≫
        (F.map f ≫ η.app b) ◁ θ.naturality g ≫
          η.naturality f ▷ (θ.app b ≫ H.map g) ≫ _ ≫
            η.app a ◁ θ.naturality f ▷ H.map g ≫ _  : _
    ... =  _ : _,
    exact (α_ _ _ _).inv,
    exact (α_ _ _ _).hom ▷ _ ≫ (α_ _ _ _).hom,
    exact _ ◁ (α_ _ _ _).hom ≫ (α_ _ _ _).inv,
    exact (α_ _ _ _).hom ≫ _ ◁ (α_ _ _ _).inv,
    exact _ ◁ (α_ _ _ _).hom ≫ (α_ _ _ _).inv,
    { rw [whisker_exchange_assoc], simp },
    { simp } } }

end oplax_nat_trans
end category_theory

[Yuma Mizuno]

The new policy is also useful in monoidal categories, although more refactors are needed.

[Yuma Mizuno]

I have two ideas for giving an associator-free proof in general bicategories.

1. Prove that equalities in bicategories can be reduced to those in strict bicategories, and write an associator-free proof in a strict bicategory.
2. Develop a tactic that automatically fills lines such as exact (α _ _ _ _) .hom ▷ _ ≫ (α _ _ _ _) .hom in the previous example. The coherence theorem guarantees that the proof works regardless of how it is filled.

Which do you think works better?

[Bhavik Mehta]

cc @Scott Morrison @Markus Himmel, we talked about this a bit for monoidal categories and I think the same ideas apply directly