Tactics/Solvers

[maxsnew]

A lot of the boring details of these proofs could be automated using domain-specific solvers. For instance this proof:

    F ⟪ f ⋆⟨ C ⟩ f' ⟫ ⋆⟨ D ⟩ (α .N-ob _ ⋆⟨ D ⟩ α' .N-ob c'')
      ≡[ i ]⟨ F .F-seq f f' i ⋆⟨ D ⟩ (α .N-ob _ ⋆⟨ D ⟩ α' .N-ob c'') ⟩
    (F ⟪ f ⟫ ⋆⟨ D ⟩ F ⟪ f' ⟫) ⋆⟨ D ⟩ (α .N-ob _ ⋆⟨ D ⟩ α' .N-ob c'')
      ≡⟨ D .⋆Assoc (F ⟪ f ⟫) (F ⟪ f' ⟫) ((α .N-ob _ ⋆⟨ D ⟩ α' .N-ob c'')) ⟩
    F ⟪ f ⟫ ⋆⟨ D ⟩ (F ⟪ f' ⟫ ⋆⟨ D ⟩ (α .N-ob _ ⋆⟨ D ⟩ α' .N-ob c''))
      ≡[ i ]⟨ F ⟪ f ⟫ ⋆⟨ D ⟩ D .⋆Assoc (F ⟪ f' ⟫) (α .N-ob _) (α' .N-ob c'') (~ i) ⟩
    F ⟪ f ⟫ ⋆⟨ D ⟩ ((F ⟪ f' ⟫ ⋆⟨ D ⟩ α .N-ob _) ⋆⟨ D ⟩ α' .N-ob c'')
      ≡[ i ]⟨ F ⟪ f ⟫ ⋆⟨ D ⟩ (α .N-hom f' i ⋆⟨ D ⟩ α' .N-ob c'') ⟩
    F ⟪ f ⟫ ⋆⟨ D ⟩ ((α .N-ob _ ⋆⟨ D ⟩ F' ⟪ f' ⟫) ⋆⟨ D ⟩ α' .N-ob c'')
      ≡[ i ]⟨ F ⟪ f ⟫ ⋆⟨ D ⟩ D .⋆Assoc (α .N-ob _) (F' ⟪ f' ⟫) (α' .N-ob c'') i ⟩
    F ⟪ f ⟫ ⋆⟨ D ⟩ (α .N-ob _ ⋆⟨ D ⟩ (F' ⟪ f' ⟫ ⋆⟨ D ⟩ α' .N-ob c''))
      ≡[ i ]⟨ D .⋆Assoc (F ⟪ f ⟫) (α .N-ob _) ((F' ⟪ f' ⟫ ⋆⟨ D ⟩ α' .N-ob c'')) (~ i) ⟩
    (F ⟪ f ⟫ ⋆⟨ D ⟩ α .N-ob c') ⋆⟨ D ⟩ (F' ⟪ f' ⟫ ⋆⟨ D ⟩ α' .N-ob c'') ∎

Is the transitive composition of 6 steps, 4 of which are just associativity.

• With a category solver consecutive associativity/identity proofs can be fused into one step and solved automatically. This would reduce the above to 4 steps, 2 of which would just be calls to a solver.
• Furthermore, if we implement a functor solver, the functoriality step could be fused additionally, giving us 1 real step (naturality) and 2 tactics.
• Finally, a natural transformation solver could automate the entire proof.

I'm going to start small and implement a category solver based on the 1lab version but using the infrastructure from cubical, used for example here.

[JacquesCarette]

Or, you know, you could borrow the combinators from agda-category (which 1lab has done) that abstract out those assocs, thus reducing the proofs back down to a more sane number of lines.

Not that shouldn't implement these solvers! Just that you don't have to suffer long annoying proofs until you get there, you can shorten them already, with well tested technology.

BTW, in interesting side-effect of doing the proofs manually with all the assocs is that moving up one level (i.e. 1 categories to 2 categories) is not so painful as you've already has to spell out things. In other words, doubling down on automation now will insure that if you go up a level, you'll find it extra painful. Your choice, of course 😄

[maxsnew]

I'm aware of these but I disagree, Jacques. Firstly, these solvers have already been implemented as well, so I just need to copy them. Secondly, for 2-categories I would write a 2-category solver.

[JacquesCarette]

Excellent - you're making an informed decision. And purposefully exploring a different part of the design space, another good thing. :+1:

[maxsnew]

Progress made: got a category solver working. Functor solver and more wouldn't be that hard tbh

[maxsnew]

Functor solver has been a much bigger task than I expected (got the formulation and construction wrong at first) but I think it's on the right track now. Biggest issue was that to avoid fiddling with a lot of transports I reformulated the UMP of the free category as a 2-categorical UMP: Any two functors out of the free category that agree up to isomorphism on generators are naturally isomorphic. There should be a stronger version of this theorem that uniquely relates those two isomorphisms but it doesn't seem needed yet for the solvers.

Here's the steps for the Functor solver. We fix phi : G -> H a graph homomorphism and we construct a functor Free phi : Free G -> Free(H+phi) where Free G is the free category on G and Free(H+phi) is something we construct explicitly:

• [X] Construct the universal interpretation: so far we have the interpretations of G in Free G and H in Free(H+phi) but need to construct the isomorphism showing the square commutes. Then for any functor F : C -> D and interpretations of G,H,phi, we can define functors from Free G to C and Free(H+phi) to D, which extend the interpretations. The last step for this proof is
• [X] Show the square we get from the semantics of the interpretations gives us a morphism from Free phi to F in the arrow category. The nat iso we need is described here.
• [x] Show that the square you get from the semantics restricts along the universal square to the interpretation square
• [ ] Show that the square that you get from the semantics is unique up to iso (in fact up to unique iso but we don't need that I think)

[maxsnew]

Implemented in https://github.com/maxsnew/multi-poly-cats/pull/15