wip: lax slices of bicategories

[plt-amy]

Implements lax slices as in §7.1 of 2-Dimensional Categories.

@aathn since you seem to have a better head on your shoulders than me when it comes to reasoning in bicategories, I'm curious if you can make out any useful patterns in the coherences I wrote in e.g. Bislice .unitor-l? A lot of of the lax functor algebra feels very reusable, but I'm struggling to see any patterns. I'm guessing you'll have run into similar shaped problems in #612 and I've just missed the helpers…

[Lavenza]

Pull request preview

New pages

• Cat.Bi.Instances.Slice (+212, -0)

Changed pages

• Cat.Bi.Base (+4, -0)
• Cat.Monoidal.Monad (± 1)

[aathn]

@plt-amy I'm glad that you speak so highly of my abilities, but as you know, I wrote a bicategory solver to avoid having to do the reasoning by hand 😅

So one answer would be that the proofs could be simplified by using the solver, for example (in unitor-l):

    snd = sym $ Hom.invertible→monic rem₁ _ _ $
      g ▶ F.₂ (B.ρ← _) ∘ g ▶ F.γ→ _ ∘ α→ _ ∘ θ₀ ◀ _ ∘ f ▶ F.υ→ ∘ ρ→ f
        ≡⟨ bicat! C ⟩
      g ▶ F.₂ (B.ρ← _) ∘ g ▶ F.γ→ _ ∘ g ▶ (_ ▶ F.υ→) ∘ α→ _ ∘ θ₀ ◀ id ∘ ρ→ f
        ≡⟨ ▶.pulll3 (F.right-unit p₀) ⟩
      g ▶ ρ← _ ∘ α→ _ ∘ θ₀ ◀ id ∘ ρ→ f
        ≡⟨ bicat! C ⟩
      θ₀
        ≡⟨ ▶.insertl (Fr.annihilate B.ρ≅.invr) ⟩
      g ▶ F.₂ (B.ρ← _) ∘ g ▶ F.₂ (B.ρ→ _) ∘ θ₀ α→ 
        ∎

If we had a solver which could also handle lax functor coherence, I think the proofs could be entirely automated. However, for one I'm not sure how to make a solver which handles lax functors (since the compositor and unitor are not invertible), and for another, I suppose this is not quite the answer you were looking for.

The helpers that I defined for #612 are in the Cat.Bi.Lax-functor.Base module of that PR:

  ▶-comp
    : ∀ {X Y Z} {f : Y B.↦ Z}
    → postaction C (₁ f) F∘ P₁ {X} {Y} => P₁ F∘ postaction B f
  ▶-comp .η x              = γ→ (_ , x)
  ▶-comp .is-natural x y α =
       CH.cdr (Fr.introl (preaction C (₁ y)) P₁.F-id)
    ∙∙ γ→nat _ _
    ∙∙ CH.car (P₁.F-∘ _ _ ∙ CH.eliml (Fr.elim P₁ B.compose.◀.F-id))

  ◀-comp
    : ∀ {X Y Z} {f : X B.↦ Y}
    → preaction C (₁ f) F∘ P₁ {Y} {Z} => P₁ F∘ preaction B f
  ◀-comp .η x              = γ→ (x , _)
  ◀-comp .is-natural x y α =
       CH.cdr (Fr.intror (postaction C (₁ x)) P₁.F-id)
    ∙∙ γ→nat _ _
    ∙∙ CH.car (P₁.F-∘ _ _ ∙ CH.elimr (Fr.elim P₁ B.compose.▶.F-id))

I think the naturality of these could probably be used to simplify bislice-compose, I see a similar pattern in the first steps of lmap .snd and rmap .snd.