open import 1Lab.Reflection.Solver
open import 1Lab.Reflection
open import 1Lab.Prelude hiding (id ; _∘_)

open import Cat.Base

open import Data.List

module Cat.Solver where

private variable
  o h : Level

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 start by defining a language of composition.

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

  private variable
    A B C : Ob

  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 What this means is that, while is some unknowable inhabitant of Hom, represents an inhabitant of Hom which is known to be a composition of (the trees that represent) and 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

  instance
    ⟦⟧-Expr : ⟦⟧-notation (Expr A B)
    ⟦⟧-Expr = brackets _ embed

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 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)

  nf : Expr A B β†’ Hom A B
  nf e = eval e id

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, by first generalising over id:

  eval-sound-k : (e : Expr B C) (f : Hom A B) β†’ eval e f ≑ ⟦ e ⟧ ∘ f
  eval-sound-k `id f = sym (idl _) -- f ≑ id ∘ f
  eval-sound-k (f `∘ g) h =
    eval f (eval g h)       β‰‘βŸ¨ eval-sound-k f _ βŸ©β‰‘
    embed f ∘ eval g h      β‰‘βŸ¨ ap (embed f ∘_) (eval-sound-k g _) βŸ©β‰‘
    embed f ∘ embed g ∘ h   β‰‘βŸ¨ assoc _ _ _ βŸ©β‰‘
    (embed f ∘ embed g) ∘ h ∎
  eval-sound-k (x ↑) f = refl -- x ∘ f ≑ x ∘ f

  eval-sound : (e : Expr A B) β†’ nf e ≑ ⟦ e ⟧
  eval-sound e = eval-sound-k e id βˆ™ idr _

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
    solve : (f g : Expr A B) β†’ nf f ≑ nf g β†’ ⟦ f ⟧ ≑ ⟦ g ⟧
    solve f g p = sym (eval-sound f) Β·Β· p Β·Β· (eval-sound g)

    solve-filler : (f g : Expr A B) β†’ (p : nf f ≑ nf g) β†’ Square (eval-sound f) p (solve f g p) (eval-sound g)
    solve-filler f g p j i = Β·Β·-filler (sym (eval-sound f)) p (eval-sound g) j i

The cursed partπŸ”—

module Reflection where

  pattern category-args xs =
    _ hm∷ _ hm∷ _ v∷ xs

  pattern β€œid” =
    def (quote Precategory.id) (category-args (_ h∷ []))

  pattern β€œβˆ˜β€ f g =
    def (quote Precategory._∘_) (category-args (_ h∷ _ h∷ _ h∷ f v∷ g v∷ []))

  mk-category-args : Term β†’ List (Arg Term) β†’ List (Arg Term)
  mk-category-args cat xs = unknown h∷ unknown h∷ cat v∷ xs

  β€œsolve” : Term β†’ Term β†’ Term β†’ Term
  β€œsolve” cat lhs rhs = def (quote NbE.solve) (mk-category-args cat $ infer-hidden 2 $ lhs v∷ rhs v∷ def (quote refl) [] v∷ [])

  β€œnf” : Term β†’ Term β†’ Term
  β€œnf” cat e = def (quote NbE.nf) (mk-category-args cat $ infer-hidden 2 $ e v∷ [])

  build-expr : Term β†’ Term
  build-expr β€œid” = con (quote NbE.`id) []
  build-expr (β€œβˆ˜β€ f g) = con (quote NbE._`∘_) (build-expr f v∷ build-expr g v∷ [] )
  build-expr f = con (quote NbE._↑) (f v∷ [])

  dont-reduce : List Name
  dont-reduce = quote Precategory.id ∷ quote Precategory._∘_ ∷ []

  cat-solver : Term β†’ SimpleSolver
  cat-solver cat .SimpleSolver.dont-reduce = dont-reduce
  cat-solver cat .SimpleSolver.build-expr tm = pure $ build-expr tm
  cat-solver cat .SimpleSolver.invoke-solver = β€œsolve” cat
  cat-solver cat .SimpleSolver.invoke-normaliser = β€œnf” cat

  repr-macro : Term β†’ Term β†’ Term β†’ TC ⊀
  repr-macro cat f _ =
    mk-simple-repr (cat-solver cat) f

  simplify-macro : Term β†’ Term β†’ Term β†’ TC ⊀
  simplify-macro cat f hole =
    mk-simple-normalise (cat-solver cat) f hole

  solve-macro : Term β†’ Term β†’ TC ⊀
  solve-macro cat hole =
    mk-simple-solver (cat-solver cat) hole

macro
  repr-cat! : Term β†’ Term β†’ Term β†’ TC ⊀
  repr-cat! cat f = Reflection.repr-macro cat f

  simpl-cat! : Term β†’ Term β†’ Term β†’ TC ⊀
  simpl-cat! cat f = Reflection.simplify-macro cat f

  cat! : Term β†’ Term β†’ TC ⊀
  cat! = Reflection.solve-macro

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 = cat! C