open import 1Lab.Reflection open import 1Lab.Prelude hiding (id ; _β_) open import Cat.Base open import Data.Bool module Cat.Solver where

# Solver for Categoriesπ

This module is split pretty cleanly into two halves: the first half implements an algorithm for reducing, in a systematic way, problems involving associativity and identity of composition in a precategory. The latter half, significantly more cursed, uses this infrastructure to automatically solve equality goals of this form.

With a precategory in hand, we by defining a language of composition.

module _ (Cat : Precategory o h) where open Precategory Cat

data Expr : Ob β Ob β Type (o β h) where `id : Expr A A _`β_ : Expr B C β Expr A B β Expr A C _β : Hom A B β Expr A B infixr 40 _`β_ infix 50 _β

A term of type Expr represents, in a symbolic way, a composite of morphisms in our category $C$. What this means is that, while $f \circ g$ is some unknowable inhabitant of Hom, $f `\circ g$ represents an inhabitant of Hom which is *known* to be a composition of (the trees that represent) $f$ and $g$. We can now define βtwoβ ways of computing the morphism that an Expr represents. The first is a straightforward embedding:

embed : Expr A B β Hom A B embed `id = id embed (f β) = f embed (f `β g) = embed f β embed g

The second computation is a bit less obvious. If youβre a programmer, it should be familiar under the name βcontinuation passing style.β Categorically, it can be seen as embedding into the presheaf category of $C$. In either case, the difference is that instead of computing a single morphism, we compute a *transformation of hom-spaces*:

eval : Expr B C β Hom A B β Hom A C eval `id f = f eval (f β) g = f β g eval (f `β g) h = eval f (eval g h) eval-sound-k : (e : Expr B C) (f : Hom A B) β eval e id β f β‘ eval e f eval-sound-k `id f = idl _ eval-sound-k (x β) f = ap (_β f) (idr x) eval-sound-k (f `β g) h = eval f (eval g id) β h β‘β¨ ap (_β h) (sym (eval-sound-k f (eval g id))) β©β‘ (eval f id β eval g id) β h β‘β¨ sym (assoc _ _ _) β©β‘ eval f id β eval g id β h β‘β¨ ap (_ β_) (eval-sound-k g h) β©β‘ eval f id β eval g h β‘β¨ eval-sound-k f _ β©β‘ eval (f `β g) h β

Working this out in a back-of-the-envelope calculation, one sees that `eval f id`

should compute the same morphism as `embed f`

. Indeed, thatβs the case! Since embed is the βintended semantics,β and eval is an βoptimised evaluator,β we call this result *soundness*. We can prove it by induction on the expression. Here are the two straightforward cases, and why they work:

eval-sound : (e : Expr A B) β eval e id β‘ embed e eval-sound `id = refl -- eval `id computes away eval-sound (x β) = idr _ -- must show f = f β id

Now comes the complicated part. First, weβll factor out proving that nested eval is the same as eval of a composition to a helper lemma. Then comes the actual inductive argument: We apply our lemma (still to be defined!), then we can apply the induction hypothesis, getting us to our goal.

eval-sound (f `β g) = eval f (eval g id) β‘β¨ sym (eval-sound-k f (eval g id)) β©β‘ eval f id β eval g id β‘β¨ apβ _β_ (eval-sound f) (eval-sound g) β©β‘ embed (f `β g) β

We now have a general theorem for solving associativity and identity problems! If two expressions compute the same transformation of hom-sets, then they represent the same morphism.

abstract associate : (f g : Expr A B) β eval f id β‘ eval g id β embed f β‘ embed g associate f g p = sym (eval-sound f) Β·Β· p Β·Β· eval-sound g

# The cursed partπ

Now we hook up associate to an Agda macro. Like all metaprogramming, itβs not pretty, but Iβve written comments around it to hopefully explain things a bit.

record CategoryNames : Type where field is-β : Name β Bool is-id : Name β Bool build-matcher : Name β Maybe Name β Name β Bool build-matcher n nothing x = n name=? x build-matcher n (just m) x = or (n name=? x) (m name=? x) find-generic-names : Name β Name β Term β TC CategoryNames find-generic-names star id mon = do β-altName β normalise (def star (unknown hβ· unknown hβ· mon vβ· [])) Ξ΅-altName β normalise (def id (unknown hβ· unknown hβ· mon vβ· [])) -- typeError (termErr β-altName β· termErr Ξ΅-altName β· []) returnTC record { is-β = build-matcher star (getName β-altName) ; is-id = build-matcher id (getName Ξ΅-altName) } find-category-names : Term β TC CategoryNames find-category-names = find-generic-names (quote Precategory._β_) (quote Precategory.id)

The trick above was stolen from the Agda standard library monoid solver. Given the term representing the category, we *evaluate* the projections (thatβs the `-altNames`

) in case they compute away to something else. This lets us not miss solutions when working with a concrete category, that might have names other than Precategory._β_ and Precategory.id.

Now we can turn to building an Expr (well, a Term representing an Expr: a representation of a representation of an arrow!) given a Term. We do this with mutual recursion, to make stuff even more complicated.

private module _ (names : CategoryNames) where open CategoryNames names build-expr : Term β Term build-β : List (Arg Term) β Term ``id : Term -- Constant representation of `id ``id = con (quote `id) [] build-expr (def x as) with is-β x | is-id x ... | false | false = con (quote _β) (def x as vβ· []) ... | false | true = ``id ... | true | q = build-β as

If weβre looking at a def (an applied defined function) or a con (an applied co/inductive constructor). If weβre looking at some random old term, then we lift it (with _β). If itβs the identity map, then we use our constant repr. of id, otherwise weβre looking at a composition.

build-expr (con x as) with is-β x | is-id x ... | false | false = con (quote _β) (def x as vβ· []) ... | false | true = ``id ... | true | q = build-β as build-expr x = con (quote _β) (x vβ· []) build-β (x vβ· y vβ· []) = con (quote _`β_) (build-expr x vβ· build-expr y vβ· []) build-β (_ β· xs) = build-β xs build-β _ = unknown get-boundary : Term β TC (Maybe (Term Γ Term)) get-boundary tm@(def (quote PathP) (_ hβ· T vβ· x vβ· y vβ· [])) = do unify tm (def (quote _β‘_) (x vβ· y vβ· [])) returnTC (just (x , y)) get-boundary _ = returnTC nothing

Then you essentially slap all of that together into a little macro.

solve-generic : (Term β TC CategoryNames) β (Term β Term) β Term β Term β TC β€ solve-generic find mkcat category hole = do goal β inferType hole >>= normalise names β find category just (lhs , rhs) β get-boundary goal where nothing β typeError (strErr "Can't solve: " β· termErr goal β· []) let rep = build-expr names unify hole (def (quote associate) (mkcat category vβ· rep lhs vβ· rep rhs vβ· def (quote refl) [] vβ· [])) macro solve : Term β Term β TC β€ solve = solve-generic find-category-names (Ξ» x β x)

## Demoπ

As a quick demonstration (and sanity check/future proofing/integration testing/what have you):

module _ (C : Precategory o h) where private module C = Precategory C variable A B : C.Ob a b c d : C.Hom A B test : a C.β (b C.β (c C.β C.id) C.β C.id C.β (d C.β C.id)) β‘ a C.β b C.β c C.β d test = solve C