Add bicategory solver and coherence lemmas

[aathn]

Description

This PR adds a solver for bicategory 2-cells, indirectly proving the coherence theorem for bicategories. It also adds a module Cat.Bi.Reasoning with some useful lemmas for bicategories including coherence lemmas.

As commented in Cat.Bi.Solver, the solver currently cannot solve goals involving the interchange law on opaque 2-cells. Support for this could be added by using the variable machinery in Reflection.Variables to sort the normal forms, but then the normal forms must be extended to explicitly represent whiskerings.

There is no prose at the moment. I figure it would be good to have prose in the end, but I didn't have time to write it yet, and wanted to make the PR first to get some feedback.

I'm not sure whether Cat.Bi.Reasoning is a good place for the coherence lemmas to live, or if they should be in Cat.Bi.Base, for example.

Checklist

Before submitting a merge request, please check the items below:

• I've read the contributing guidelines.
• The imports of new modules have been sorted with support/sort-imports.hs (or nix run --experimental-features nix-command -f . sort-imports).
• All new code blocks have "agda" as their language.

If your change affects many files without adding substantial content, and
you don't want your name to appear on those pages (for example, treewide
refactorings or reformattings), start the commit message and PR title with chore:.

[Lavenza]

Pull request preview

[plt-amy]

(I haven't looked at the code yet)

I'm not sure whether Cat.Bi.Reasoning is a good place for the coherence lemmas to live, or if they should be in Cat.Bi.Base, for example.

Cat.Bi.Base is already a nightmare module so let's not put anything else in there.

[aathn]

I realized it should be possible to handle the interchange law without involving any variables, by just placing left whiskerings before right ones, basically. I might give it a try, but it would require fairly big changes to the representation of normal forms

[aathn]

I realized it should be possible to handle the interchange law without involving any variables

I have implemented this now, and it seems to be working well. Unfortunately, the soundness proofs for the new additions (especially the function frame-compare) seem to take a lot of resources to check, and the whole file takes about 10G more to check now than it did before. I would be grateful for any advise on how to improve the performance.

[aathn]

Teaser of the solver in action, when defining the composition of lax transformations:

lx .ν-compositor {a = a} {b} {c} f g =
  ν .η (f B.⊗ g) ∘ H.γ→ f g ◀ (α.σ a ⊗ β.σ a)                          ≡⟨ bicat! C ⟩
  α← _ _ _ ∘ α.σ c ▶ β.ν→ (f B.⊗ g) ∘ α→ _ _ _
  ∘ ⌜ α.ν→ (f B.⊗ g) ∘ H.γ→ f g ◀ α.σ a ⌝ ◀ β.σ a ∘ α← _ _ _           ≡⟨ ap! (α.ν-compositor f g) ⟩
  α← _ _ _ ∘ α.σ c ▶ β.ν→ (f B.⊗ g) ∘ α→ _ _ _
  ∘ (α.σ c ▶ G.γ→ f g ∘ α→ _ _ _ ∘ α.ν→ f ◀ G.₁ g
    ∘ α← _ _ _ ∘ H.₁ f ▶ α.ν→ g ∘ α→ _ _ _) ◀ β.σ a ∘ α← _ _ _         ≡⟨ bicat! C ⟩
  α← _ _ _ ∘ α.σ c ▶ ⌜ β.ν→ (f B.⊗ g) ∘ G.γ→ f g ◀ β.σ a ⌝ ∘ α→ _ _ _
  ∘ α→ _ _ _ ◀ β.σ a ∘ (α.ν→ f ◀ G.₁ g) ◀ β.σ a ∘ α← _ _ _ ◀ β.σ a
  ∘ (H.₁ f ▶ α.ν→ g) ◀ β.σ a ∘ α→ _ _ _ ◀ β.σ a ∘ α← _ _ _             ≡⟨ ap! (β.ν-compositor f g) ⟩
  α← _ _ _ ∘ α.σ c ▶
    (β.σ c ▶ F.γ→ f g ∘ α→ _ _ _ ∘ β.ν→ f ◀ F.₁ g
    ∘ α← _ _ _ ∘ G.₁ f ▶ β.ν→ g ∘ α→ _ _ _) ∘ α→ _ _ _
  ∘ α→ _ _ _ ◀ β.σ a ∘ (α.ν→ f ◀ G.₁ g) ◀ β.σ a ∘ α← _ _ _ ◀ β.σ a
  ∘ (H.₁ f ▶ α.ν→ g) ◀ β.σ a ∘ α→ _ _ _ ◀ β.σ a ∘ α← _ _ _             ≡⟨ bicat! C ⟩
  (α.σ c ⊗ β.σ c) ▶ F.γ→ f g ∘ α→ _ _ _ ∘ ν .η f ◀ F.₁ g
  ∘ α← _ _ _ ∘ H.₁ f ▶ ν .η g ∘ α→ _ _ _                               ∎

Not wanting to do these by hand is what prompted me to write this solver 😅

[plt-amy]

I would be grateful for any advise on how to improve the performance.

@aathn Unfortunately most of the overhead seems to be from the cubical parts of the coverage checker (inventing clauses for the trX constructors inserted to make transport work in indexed types). This is something that can be avoided, but it's going to be annoying: you have to put everything in Typeω. This is agda --profile=definitions src/Cat/Bi/Solver.agda, as you have written it, commenting out everything after frame-compare:

Checking Cat.Bi.Solver (/home/amelia/default/Projects/1lab.dev/src/Cat/Bi/Solver.agda).
Total                               8,077ms 
Miscellaneous                       3,464ms 
Cat.Bi.Solver.NbE.frame-compare     3,096ms 
Cat.Bi.Solver.NbE.`whisker            379ms 
Cat.Bi.Solver.NbE.embed₂              333ms 
Cat.Bi.Solver.NbE.eval₂               268ms 
Cat.Bi.Solver.NbE.val₂-embed          183ms 
Cat.Bi.Solver.NbE.frame-embed         176ms 
Cat.Bi.Solver.NbE.eval₁-sound          38ms 
Cat.Bi.Solver.NbE.`eval₁-sound-to      29ms 
Cat.Bi.Solver.NbE.`eval₁-sound-from    29ms 
Cat.Bi.Solver.NbE.Expr₂                29ms 
Cat.Bi.Solver.NbE.Frame                23ms 
Cat.Bi.Solver.NbE.eval₁                12ms 
Cat.Bi.Solver.NbE.embed₁               12ms

But if we make the necessary changes so that Frame can be in Typeω instead:

Checking Cat.Bi.Solver (/home/amelia/default/Projects/1lab.dev/src/Cat/Bi/Solver.agda).
Total                               1,688ms 
Miscellaneous                         989ms 
Cat.Bi.Solver.NbE.frame-compare       400ms
[...]

I'll do the rest of the work and toss you a patch in a bit.

[plt-amy]

Here: https://gist.github.com/plt-amy/14b0587e2f9093ade7a40ffb6b7336b1

$ curl https://gist.githubusercontent.com/plt-amy/14b0587e2f9093ade7a40ffb6b7336b1/raw/7d5ef2f61cb1b04308a09b3e8d3dadb57a36e47d/0001-chore-put-bicategory-solver-types-in-Type.patch | git am -

The next worst thing is the definition of build… I think you're running into some stupid quadratic case of the coverage checker, or something like that. Commoning up all the cases with “η” cuts checking that one function from 6s to 0.821s, and removing the overly-specific arguments to like the “id” pattern synonym cuts it down in half again: https://gist.github.com/plt-amy/6e3451c3b9dcb733b26a8f2aa2c88900

$ curl https://gist.githubusercontent.com/plt-amy/6e3451c3b9dcb733b26a8f2aa2c88900/raw/a3fb93e1bec3e41457fae8c65e24ff5b302e8ba2/0001-chore-better-matching-perf.-in-build.patch | git am -

[plt-amy]

Also looking at your code sample makes me think that we should probably make λ← etc take implicit arguments, lol.

[aathn]

@plt-amy That's amazing, thank you! A question: I thought SSet serves the exact purpose we need here, being a non-fibrant version of Type (and indeed, using SSet also seems to improve the checking time). How come you prefer using Typeω, is it just to minimize the dependency on --two-level?

[plt-amy]

I find that whenever I try to cram things into SSet it ends up upsetting the pattern-matching checker ("can not split on fibrant type Foo unless target type is also fibrant"), so I just default to Typeω now.

[aathn]

I see! I changed to SSet now just because it felt slightly more principled to me, but I am happy to revert it if you think that's better.

[plt-amy]

This is pretty fantastic work, thank you! I think I'm still going to wait for @TOTBWF's opinion on the evaluation strategy since he's the solver expert, but this looks great to me.

I'm fine with either SSet or Typeω. (Also, I was kinda just doing the Typeω refactor on autopilot, so I might've missed some style-guide nitpicks… Sorry.)

[aathn]

Also looking at your code sample makes me think that we should probably make λ← etc take implicit arguments, lol.

I'm not sure, for pedagogical purposes I think it's often better for them to be explicit, although of course it clutters things when you have a big goal. Something that would certainly make it more convenient to work with bicategories is to make λ← etc the primitive fields, and then have the composition functor and natural isomorphisms be derived instead. That way, normalising a goal would give something way more readable. But of course, that would be a very invasive change, and it would be inconsistent with how things are defined elsewhere in the library.

[plt-amy]

Also,

There is no prose at the moment. I figure it would be good to have prose in the end, but I didn't have time to write it yet, and wanted to make the PR first to get some feedback.

I think our position is that the reflection code is exempt from prose requirements, but, since this solver does basically prove something nontrivial about bicategories (coherence), it might still be a good idea to have it.

Something that would certainly make it more convenient to work with bicategories is to make λ← etc the primitive fields [...]

Yeah, we've also considered this in the past. It feels kinda nasty, but I think everything past and including the composition functor probably needs to be exploded. For now, we can improve on the display of λ and ρ by changing the definition of the λ← _ (etc.) abbreviations to this:

  module unitor-l {a} {b} = Cr._≅_ _ (unitor-l {a} {b})
  module unitor-r {a} {b} = Cr._≅_ _ (unitor-r {a} {b})
  private
    open module λ← {a b} = _=>_ (unitor-l.from {a} {b}) renaming (η to λ←) using () public
    open module λ→ {a b} = _=>_ (unitor-l.to   {a} {b}) renaming (η to λ→) using () public
    open module ρ← {a b} = _=>_ (unitor-r.from {a} {b}) renaming (η to ρ←) using () public
    open module ρ→ {a b} = _=>_ (unitor-r.to   {a} {b}) renaming (η to ρ→) using () public

Everything that takes a tuple is sorta beyond what we can solve without changes upstream.

[plt-amy]

Well, I mean, you can also replace α← and α→ with

    open module α→ {a b c d} = _=>_ (associator.to {a} {b} {c} {d})   renaming (η to α→) using () public
    open module α← {a b c d} = _=>_ (associator.from {a} {b} {c} {d}) renaming (η to α←) using () public

but this requires making it take a tuple argument everywhere (on the bright side, α← _ _ _ becomes α← _?). Making the fields of the compose functor display infix is impossible ATM, but perhaps that means the composition functor is the only thing we need to explode.

[TOTBWF]

This is amazing, thank you! I did have some high-level questions about the code, especially the frame stuff.

[plt-amy]

@aathn Can you add a test case for the situation described in your latest commit, something that passes only with this ordering from frame-compare?