open import 1Lab.Reflection

open import Cat.Diagram.Product
open import Cat.Prelude

open import Data.List

import Cat.Reasoning
module Cat.Diagram.Product.Solver where

A solver for categories with binary productsπŸ”—

Much like the category solver, this module is split into two halves. The first implements an algorithm for normalizing expressions in the language of a category with binary products. The latter half consists of the usual reflection hacks required to transform Agda expressions into our internal expression type.

module NbE {o β„“} (π’ž : Precategory o β„“) (cartesian : βˆ€ A B β†’ Product π’ž A B) where
  open Cat.Reasoning π’ž
  open Binary-products π’ž cartesian

ExpressionsπŸ”—

We begin by defining an expression type for a category with binary products. Mathematically, this /almost/ corresponds to the free category with binary products over a quiver, but we are working with un-quotiented syntax.

  data •Ob• : Type (o βŠ” β„“) where
    _β€ΆβŠ—β€Ά_ : •Ob• β†’ •Ob• β†’ •Ob•
    •_•   : Ob β†’ •Ob•

  ⟦_βŸ§β‚’ : •Ob• β†’ Ob
  ⟦ X β€ΆβŠ—β€Ά Y βŸ§β‚’ =  ⟦ X βŸ§β‚’ βŠ—β‚€ ⟦ Y βŸ§β‚’
  ⟦ • X • βŸ§β‚’ = X

  data Expr : •Ob• β†’ •Ob• β†’ Type (o βŠ” β„“) where
    •id•    : βˆ€ {X} β†’ Expr X X
    _β€Άβˆ˜β€Ά_   : βˆ€ {X Y Z} β†’ Expr Y Z β†’ Expr X Y β†’ Expr X Z
    •π₁•    : βˆ€ {X Y} β†’ Expr (X β€ΆβŠ—β€Ά Y) X
    •π₂•    : βˆ€ {X Y} β†’ Expr (X β€ΆβŠ—β€Ά Y) Y
    β€ΆβŸ¨_,_βŸ©β€Ά : βˆ€ {X Y Z} β†’ Expr X Y β†’ Expr X Z β†’ Expr X (Y β€ΆβŠ—β€Ά Z)
    •_•     : βˆ€ {X Y} β†’ Hom ⟦ X βŸ§β‚’ ⟦ Y βŸ§β‚’ β†’ Expr X Y

Note that we also define a syntax for products of objects in this free category, even though the ambient category π’ž already has binary products. The reason for this is two-fold. The first, more mundane reason is that the unifier will get very confused if we don’t do this. The second reason is much more mathematically interesting, as it pertains to our choice of normalization algorithm.

Much like the aforementioned category solver, we are going to be using a variant of Normalization By Evaluation (NbE for short). This class of normalization algorithms operates by constructing a domain of β€œvalues”, which are meant to denote the semantics of some expression. Normalization then occurs in 2 phases: an β€œevaluation” phase where we transform expressions into values, and a β€œquotation” phase where we reflect values back into expressions. As the values are meant to represent the semantics of an expression, each equivalence class of expressions ought to be mapped to the same value during evaluation. The quotation phase then plucks out a canonical representative for each one of these equivalence classes, which then becomes our normal form.

The particular variant of NbE that we are using is known as Typed NbE. What distinguishes it from Untyped NbE is the treatment of quotation. In Untyped NbE, quotation proceeds in a syntax-directed manner, which makes the enaction of Ξ·-laws1 more difficult. On the other hand, if we quote in a type directed manner, we can perform Ξ·-expansion at every possible opportunity, which simplifies the implementation considerably. This will result in larger normal forms, but the expressions the solver needs to deal with are small, so this isn’t a pressing issue.

Next, we define an interpretation of expressions back into morphisms. This will be used to state the all-important soundness theorem.

  ⟦_βŸ§β‚‘ : βˆ€ {X Y} β†’ Expr X Y β†’ Hom ⟦ X βŸ§β‚’ ⟦ Y βŸ§β‚’
  ⟦ •id• βŸ§β‚‘ = id
  ⟦ e1 β€Άβˆ˜β€Ά e2 βŸ§β‚‘ = ⟦ e1 βŸ§β‚‘ ∘ ⟦ e2 βŸ§β‚‘
  ⟦ •π₁• βŸ§β‚‘ = π₁
  ⟦ •π₂• βŸ§β‚‘ = Ο€β‚‚
  ⟦ β€ΆβŸ¨ e1 , e2 βŸ©β€Ά βŸ§β‚‘ = ⟨ ⟦ e1 βŸ§β‚‘ , ⟦ e2 βŸ§β‚‘ ⟩
  ⟦ • f • βŸ§β‚‘ = f

ValuesπŸ”—

Next, we define a type of Values. The goal here is to ensure that we can’t have any eliminators (in our case, projections) applied to introduction forms (in our case, ⟨_,_⟩). We also need to handle the normal associativity/identity equations, but those will be handled by evaluating our expressions into presheaves.

  data Value : •Ob• β†’ •Ob• β†’ Type (o βŠ” β„“) where
    vhom  : βˆ€ {X Y} β†’ Hom ⟦ X βŸ§β‚’ ⟦ Y βŸ§β‚’ β†’ Value X Y
    vpair : βˆ€ {X Y Z} β†’ Value X Y β†’ Value X Z β†’ Value X (Y β€ΆβŠ—β€Ά Z)

We now define our eliminators for values.

  vfst : βˆ€ {X Y Z} β†’ Value X (Y β€ΆβŠ—β€Ά Z) β†’ Value X Y
  vfst (vhom f) = vhom (π₁ ∘ f)
  vfst (vpair v1 v2) = v1

  vsnd : βˆ€ {X Y Z} β†’ Value X (Y β€ΆβŠ—β€Ά Z) β†’ Value X Z
  vsnd (vhom f) = vhom (Ο€β‚‚ ∘ f)
  vsnd (vpair v1 v2) = v2

  vid : βˆ€ {X} β†’ Value X X
  vid = vhom id

QuotationπŸ”—

As noted above, our quotation is type-directed to make applying Ξ·-laws easier. When we encounter a v : Value X (Y β€ΆβŠ—β€Ά Z), we will always Ξ·-expand it using the eliminators defined above. If v is a vpair, then the eliminators will compute away, and we will be left with the same value we started with. If v is a vhom, then we will have Ξ·-expanded it, so all of our normal forms will be /fully/ Ξ·-expanded.

As a terminological note, we call this function reflect because quote is a reserved keyword in Agda.

  reflect : βˆ€ X Y β†’ Value X Y β†’ Hom ⟦ X βŸ§β‚’ ⟦ Y βŸ§β‚’
  reflect X (Y β€ΆβŠ—β€Ά Z) v = ⟨ (reflect X Y (vfst v)) , reflect X Z (vsnd v) ⟩
  reflect X • Y • (vhom f) = f

EvaluationπŸ”—

Evaluation operates in much the same way as the category solver, where we evaluate to Value X Y β†’ Value X Z instead of just Value Y Z. This allows us to apply the associativity/identity equations, as well as the equation that ⟨ f , g ⟩ ∘ h ≑ ⟨ f ∘ h , g ∘ h ⟩.

  eval : βˆ€ {X Y Z} β†’ Expr Y Z β†’ Value X Y β†’ Value X Z
  eval •id• v = v
  eval (e1 β€Άβˆ˜β€Ά e2) v = eval e1 (eval e2 v)
  eval •π₁• v = vfst v
  eval •π₂• v = vsnd v
  eval β€ΆβŸ¨ e1 , e2 βŸ©β€Ά v = vpair (eval e1 v) (eval e2 v)
  eval • f • v = vhom (f ∘ reflect _ _ v)

As noted earlier, we obtain normal forms by evaluating then quoting.

  nf : βˆ€ X Y β†’ Expr X Y β†’ Hom ⟦ X βŸ§β‚’ ⟦ Y βŸ§β‚’
  nf X Y e = reflect X Y (eval e vid)

SoundnessπŸ”—

Before proving soundness, we need to prove the normal battery of random lemmas. The first states that quoting a vhom f gives us back f.

  vhom-sound : βˆ€ X Y β†’ (f : Hom ⟦ X βŸ§β‚’ ⟦ Y βŸ§β‚’) β†’ reflect X Y (vhom f) ≑ f
  vhom-sound X (Y β€ΆβŠ—β€Ά Z) f =
    ⟨ reflect X Y (vhom (π₁ ∘ f)) , reflect X Z (vhom (Ο€β‚‚ ∘ f)) ⟩ β‰‘βŸ¨ apβ‚‚ ⟨_,_⟩ (vhom-sound X Y (π₁ ∘ f)) (vhom-sound X Z (Ο€β‚‚ ∘ f)) ⟩
    ⟨ π₁ ∘ f , Ο€β‚‚ ∘ f ⟩                                           β‰‘Λ˜βŸ¨ ⟨⟩-unique refl refl ⟩
    f                                                             ∎
  vhom-sound X • x • f = refl

Next, some soundless lemmas for our eliminators. We want to show that applying each eliminator to a value corresponds to the correct thing once interpreted into our category π’ž.

  vfst-sound : βˆ€ X Y Z β†’ (v : Value X (Y β€ΆβŠ—β€Ά Z)) β†’ reflect X Y (vfst v) ≑ π₁ ∘ reflect X (Y β€ΆβŠ—β€Ά Z) v
  vfst-sound X Y Z (vhom f) =
    reflect X Y (vhom (π₁ ∘ f))       β‰‘βŸ¨ vhom-sound X Y (π₁ ∘ f) ⟩
    π₁ ∘ f                            β‰‘Λ˜βŸ¨ refl⟩∘⟨ vhom-sound X (Y β€ΆβŠ—β€Ά Z) f ⟩
    π₁ ∘ reflect X (Y β€ΆβŠ—β€Ά Z) (vhom f) ∎
  vfst-sound X Y Z (vpair v1 v2) =
    reflect X Y v1                               β‰‘Λ˜βŸ¨ Ο€β‚βˆ˜βŸ¨βŸ© ⟩
    π₁ ∘ ⟨ (reflect X Y v1) , (reflect X Z v2) ⟩ ∎

  vsnd-sound : βˆ€ X Y Z β†’ (v : Value X (Y β€ΆβŠ—β€Ά Z)) β†’ reflect X Z (vsnd v) ≑ Ο€β‚‚ ∘ reflect X (Y β€ΆβŠ—β€Ά Z) v
  vsnd-sound X Y Z (vhom f) =
    reflect X Z (vhom (Ο€β‚‚ ∘ f))       β‰‘βŸ¨ vhom-sound X Z (Ο€β‚‚ ∘ f) ⟩
    Ο€β‚‚ ∘ f                            β‰‘Λ˜βŸ¨ refl⟩∘⟨ vhom-sound X (Y β€ΆβŠ—β€Ά Z) f ⟩
    Ο€β‚‚ ∘ reflect X (Y β€ΆβŠ—β€Ά Z) (vhom f) ∎
  vsnd-sound X Y Z (vpair v1 v2) =
    reflect X Z v2                               β‰‘Λ˜βŸ¨ Ο€β‚‚βˆ˜βŸ¨βŸ© ⟩
    Ο€β‚‚ ∘ ⟨ (reflect X Y v1) , (reflect X Z v2) ⟩ ∎

We handle composition of values by interpreting expressions as functions /between/ values. So in a sense, this following lemma is a proof of soundness for our interpretation of composition.

  sound-k : βˆ€ X Y Z β†’ (e : Expr Y Z) β†’ (v : Value X Y)
          β†’ reflect X Z (eval e v) ≑ ⟦ e βŸ§β‚‘ ∘ reflect X Y v
  sound-k X Y Y •id• v = sym (idl _)
  sound-k X Y Z (e1 β€Άβˆ˜β€Ά e2) v =
    reflect X Z (eval e1 (eval e2 v)) β‰‘βŸ¨ sound-k X _ Z e1 (eval e2 v) ⟩
    ⟦ e1 βŸ§β‚‘ ∘ reflect X _ (eval e2 v) β‰‘βŸ¨ refl⟩∘⟨ sound-k X Y _ e2 v ⟩
    ⟦ e1 βŸ§β‚‘ ∘ ⟦ e2 βŸ§β‚‘ ∘ reflect X Y v β‰‘βŸ¨ assoc _ _ _ ⟩
    ⟦ e1 β€Άβˆ˜β€Ά e2 βŸ§β‚‘ ∘ reflect X Y v    ∎
  sound-k X (Y β€ΆβŠ—β€Ά Z) Y •π₁• v = vfst-sound X Y Z v
  sound-k X (Y β€ΆβŠ—β€Ά Z) Z •π₂• v = vsnd-sound X Y Z v
  sound-k X Y (Z1 β€ΆβŠ—β€Ά Z2) β€ΆβŸ¨ e1 , e2 βŸ©β€Ά v =
    ⟨ reflect X Z1 (eval e1 v) , reflect X Z2 (eval e2 v) ⟩ β‰‘βŸ¨ apβ‚‚ ⟨_,_⟩ (sound-k X Y Z1 e1 v) (sound-k X Y Z2 e2 v) ⟩
    ⟨ ⟦ e1 βŸ§β‚‘ ∘ reflect X Y v , ⟦ e2 βŸ§β‚‘ ∘ reflect X Y v ⟩   β‰‘Λ˜βŸ¨ ⟨⟩∘ _ ⟩
    ⟨ ⟦ e1 βŸ§β‚‘ , ⟦ e2 βŸ§β‚‘ ⟩ ∘ reflect X Y v                   ∎
  sound-k X Y Z • x • v = vhom-sound X Z _

The final soundness proof: normalizing an expression gives us the same morphism as naively interpreting the expression.

  sound : βˆ€ X Y β†’ (e : Expr X Y) β†’ nf X Y e ≑ ⟦ e βŸ§β‚‘
  sound X Y e = sound-k X X Y e vid βˆ™ elimr (vhom-sound X X id)

Solver interfaceπŸ”—

In order to make the reflection easier later, we bundle up the soundness proof. Marking this as abstract is very important. This prevents agda from unfolding into an absolutely enormous proof when used as a macro, which is critical for performance.

  abstract
    solve : βˆ€ X Y β†’ (e1 e2 : Expr X Y) β†’ nf X Y e1 ≑ nf X Y e2 β†’ ⟦ e1 βŸ§β‚‘ ≑ ⟦ e2 βŸ§β‚‘
    solve X Y e1 e2 p = sym (sound X Y e1) βˆ™βˆ™ p βˆ™βˆ™ sound X Y e2

ReflectionπŸ”—

As per usual, this is the hard part. Reflection is normally quite tricky, but the situation here is even harder than the category solver, as we need to reflect on objects as well as morphisms.

We begin by defining a bunch of pattern synonyms for matching on various fields of precategories, as well as objects + morphisms that arise from the product structure.

The situation here is extremely fiddly when it comes to implicit arguments, as we not only need to get the number correct, but also their multiplicity. Record projections always mark the records parameters as hidden and quantity-0, so we need to take care to do the same in these patterns.

module Reflection where
  private
    pattern is-product-field X Y args =
      _ hm∷ _ hm∷ _ hm∷ -- category args
      X hm∷ Y hm∷       -- objects of product
      _ hm∷             -- apex
      _ hm∷ _ hm∷       -- projections
      _ v∷              -- is-product record argument
      args
    pattern product-field X Y args =
      _ hm∷ _ hm∷ _ hm∷ -- category args
      X hm∷ Y hm∷       -- objects of product
      _ v∷              -- product record argument
      args
    pattern category-field args = _ hm∷ _ hm∷ _ v∷ args

    pattern β€œβŠ—β€ X Y =
      def (quote Product.apex) (product-field X Y [])
    pattern β€œid” X =
      def (quote Precategory.id) (category-field (X h∷ []))
    pattern β€œβˆ˜β€ X Y Z f g =
      def (quote Precategory._∘_) (category-field (X h∷ Y h∷ Z h∷ f v∷ g v∷ []))
    pattern β€œΟ€β‚β€ X Y =
      def (quote (Product.π₁)) (product-field X Y [])
    pattern β€œΟ€β‚‚β€ X Y =
      def (quote (Product.Ο€β‚‚)) (product-field X Y [])
    pattern β€œβŸ¨βŸ©β€ X Y Z f g =
      def (quote (is-product.⟨_,_⟩)) (is-product-field Y Z (X h∷ f v∷ g v∷ []))

Next, we define some helpers to make constructing things in the NbE module easier.

    mk-nbe-con : Name β†’ List (Arg Term) β†’ Term
    mk-nbe-con con-name args =
      con con-name (unknown h∷ unknown h∷ unknown h∷ unknown h∷ args)

    mk-nbe-call : Term β†’ Term β†’ List (Arg Term) β†’ List (Arg Term)
    mk-nbe-call cat cart args = unknown h∷ unknown h∷ cat v∷ cart v∷ args

We also define some helpers for building quoted calls to NbE.nf and NbE.solve.

  β€œnf” : Term β†’ Term β†’ Term β†’ Term β†’ Term β†’ Term
  β€œnf” cat cart x y e =
    def (quote NbE.nf) (mk-nbe-call cat cart (x v∷ y v∷ e v∷ []))

  β€œsolve” : Term β†’ Term β†’ Term β†’ Term β†’ Term β†’ Term β†’ Term
  β€œsolve” cat cart x y lhs rhs =
    def (quote NbE.solve) $
      mk-nbe-call cat cart (x v∷ y v∷ lhs v∷ rhs v∷ β€œrefl” v∷ [])

Now for the meat of the reflection. build-obj-expr will construct quoted terms of type NbE.•Ob• from quoted terms of type Precategory.Ob. build-hom-expr does the same thing, but for NbE.Expr and Precategory.Hom.

Note that we apply all implicits to constructors in build-hom-expr. If we don’t do this, Agda will get very upset.

  build-obj-expr : Term β†’ Term
  build-obj-expr (β€œβŠ—β€ X Y)  =
    con (quote NbE.•Ob•._β€ΆβŠ—β€Ά_) (build-obj-expr X v∷ build-obj-expr Y v∷ [])
  build-obj-expr X =
    con (quote NbE.•Ob•.•_•) (X v∷ [])

  build-hom-expr : Term β†’ Term
  build-hom-expr (β€œid” X) =
    mk-nbe-con (quote NbE.Expr.•id•) $
      build-obj-expr X h∷ []
  build-hom-expr (β€œβˆ˜β€ X Y Z f g) =
    mk-nbe-con (quote NbE.Expr._β€Άβˆ˜β€Ά_) $
      build-obj-expr X h∷ build-obj-expr Y h∷ build-obj-expr Z h∷
      build-hom-expr f v∷ build-hom-expr g v∷ []
  build-hom-expr (β€œΟ€β‚β€ X Y) =
    mk-nbe-con (quote NbE.Expr.•π₁•) $
      build-obj-expr X h∷ build-obj-expr Y h∷ []
  build-hom-expr (β€œΟ€β‚‚β€ X Y) =
    mk-nbe-con (quote NbE.Expr.•π₂•) $
      build-obj-expr X h∷ build-obj-expr Y h∷ []
  build-hom-expr (β€œβŸ¨βŸ©β€ X Y Z f g) =
    mk-nbe-con (quote NbE.Expr.β€ΆβŸ¨_,_βŸ©β€Ά) $
    build-obj-expr X h∷ build-obj-expr Y h∷ build-obj-expr Z h∷
    build-hom-expr f v∷ build-hom-expr g v∷ []
  build-hom-expr f =
    con (quote NbE.Expr.•_•) (f v∷ [])

Now, for the solver interface. This follows the usual pattern: we create a list of names that we will pass to withReduceDefs, which will prevent Agda from normalizing away the things we want to reflect upon.

  dont-reduce : List Name
  dont-reduce =
    quote Precategory.Hom ∷
    quote Precategory.id ∷
    quote Precategory._∘_ ∷
    quote Product.apex ∷
    quote Product.π₁ ∷
    quote Product.Ο€β‚‚ ∷
    quote is-product.⟨_,_⟩ ∷ []

We will need to recover the objects from some quoted hom to make the calls to the solver/normaliser.

  get-objects : Term β†’ TC (Term Γ— Term)
  get-objects tm = ((infer-type tm >>= normalise) >>= wait-just-a-bit) >>= Ξ» where
    (def (quote Precategory.Hom) (category-field (x v∷ y v∷ []))) β†’
      pure (x , y)
    tp β†’
      typeError $ strErr "Can't determine objects: " ∷ termErr tp ∷ []

We also make some debugging macros, which are very useful for when you want to examine the exact quoted representations of objects/homs.

  obj-repr-macro : βˆ€ {o β„“} (π’ž : Precategory o β„“) (cartesian : βˆ€ X Y β†’ Product π’ž X Y) β†’ Term β†’ Term β†’ TC ⊀
  obj-repr-macro cat cart hom hole =
    withReconstructed true $
    withNormalisation false $
    withReduceDefs (false , dont-reduce) $ do
    (x , y) ← get-objects hom
    β€œx” ← build-obj-expr <$> normalise x
    β€œy” ← build-obj-expr <$> normalise y
    typeError $ strErr "Determined objects of " ∷ termErr hom ∷ strErr " to be\n  " ∷
                termErr x ∷ strErr "\nAnd\n  " ∷
                termErr y ∷ strErr "\nWith quoted representations\n  " ∷
                termErr β€œx” ∷ strErr "\nAnd\n  " ∷
                termErr β€œy” ∷ []

  hom-repr-macro : βˆ€ {o β„“} (π’ž : Precategory o β„“) (cartesian : βˆ€ X Y β†’ Product π’ž X Y) β†’ Term β†’ Term β†’ TC ⊀
  hom-repr-macro cat cart hom hole =
    withReconstructed true $
    withNormalisation false $
    withReduceDefs (false , dont-reduce) $ do
    (x , y) ← get-objects hom
    β€œx” ← build-obj-expr <$> normalise x
    β€œy” ← build-obj-expr <$> normalise y
    β€œhom” ← build-hom-expr <$> normalise hom
    typeError $ strErr "The morphism\n  " ∷
                termErr hom ∷ strErr "\nis represented by\n  " ∷
                termErr β€œhom” ∷ strErr "\nwith objects\n  " ∷
                termErr β€œx” ∷ strErr "\nAnd\n  " ∷
                termErr β€œy” ∷ []

Now, the simplifier and solver reflection. This just puts together all of our bits from before.

There is one subtlety here with regards to withReconstructed. We are reflecting on the record parameters to Product and is-product to determine the objects involved in things like ⟨_,_⟩, which Agda will mark as unknown by default. This will cause build-obj-expr to then fail when we have expressions involving nested _βŠ—_. Wrapping everything in withReconstructed causes Agda to fill in these arguments with their actual values, which then fixes the issue.

  simpl-macro : βˆ€ {o β„“} (π’ž : Precategory o β„“) (cartesian : βˆ€ X Y β†’ Product π’ž X Y) β†’ Term β†’ Term β†’ TC ⊀
  simpl-macro cat cart hom hole =
    withReconstructed true $
    withNormalisation false $
    withReduceDefs (false , dont-reduce) $ do
    (x , y) ← get-objects hom
    β€œx” ← build-obj-expr <$> normalise x
    β€œy” ← build-obj-expr <$> normalise y
    β€œhom” ← build-hom-expr <$> normalise hom
    β€œcat” ← quoteTC cat
    β€œcart” ← quoteTC cart
    unify hole (β€œnf” β€œcat” β€œcart” β€œx” β€œy” β€œhom”)

Finally, we define the user-facing interface as a series of macros.

macro
  products-obj-repr! : βˆ€ {o β„“}
                       β†’ (π’ž : Precategory o β„“) (cartesian : βˆ€ X Y β†’ Product π’ž X Y)
                       β†’ Term β†’ Term β†’ TC ⊀
  products-obj-repr! = Reflection.obj-repr-macro

  products-repr! : βˆ€ {o β„“}
                   β†’ (π’ž : Precategory o β„“) (cartesian : βˆ€ X Y β†’ Product π’ž X Y)
                   β†’ Term β†’ Term β†’ TC ⊀
  products-repr! = Reflection.hom-repr-macro

  products-simpl! : βˆ€ {o β„“}
                    β†’ (π’ž : Precategory o β„“) (cartesian : βˆ€ X Y β†’ Product π’ž X Y)
                    β†’ Term β†’ Term β†’ TC ⊀
  products-simpl! = Reflection.simpl-macro
module _ {o β„“} {C : Precategory o β„“} (cart : βˆ€ X Y β†’ Product C X Y) {x y : ⌞ C ⌟} {h1 h2 : C .Precategory.Hom x y} where
  open Reflection

  private
    products-worker : Term β†’ TC ⊀
    products-worker goal = withReconstructed true $ withNormalisation true $ withReduceDefs (false , dont-reduce) do
      `h1 ← wait-for-type =<< quoteTC h1
      `h2 ← quoteTC h2
      `x ← quoteTC x
      `y ← quoteTC y

      β€œcart” ← quoteTC cart

      let
        β€œx”   = build-obj-expr `x
        β€œy”   = build-obj-expr `y
        β€œlhs” = build-hom-expr `h1
        β€œrhs” = build-hom-expr `h2

      unify goal (Reflection.β€œsolve” unknown β€œcart” β€œx” β€œy” β€œlhs” β€œrhs”) <|> do
        β€œcat” ← quoteTC C
        vlhs ← normalise (β€œnf” β€œcat” β€œcart” β€œx” β€œy” β€œlhs”)
        vrhs ← normalise (β€œnf” β€œcat” β€œcart” β€œx” β€œy” β€œrhs”)
        typeError
          [ "Could not equate the following expressions:\n  "
          , termErr `h1 , "\nAnd\n  " , termErr `h2
          , "\nReflected expressions\n  "
          , termErr β€œlhs” , "\nAnd\n  " , termErr β€œrhs”
          , strErr "\nComputed normal forms\n  "
          , termErr vlhs , strErr "\nAnd\n  " , termErr vrhs
          ]

  products-wrapper : {@(tactic products-worker) p : h1 ≑ h2} β†’ h1 ≑ h2
  products-wrapper {p = p} = p

macro
  products! : Term β†’ TC ⊀
  products! = flip unify (def (quote products-wrapper) [])

DemoπŸ”—

Wow, that was a lot of hard work! Let’s marvel at the fruits of our labor.

private module Tests {o β„“} (π’ž : Precategory o β„“) (cartesian : βˆ€ X Y β†’ Product π’ž X Y) where
  open Precategory π’ž
  open Binary-products π’ž cartesian
  open NbE π’ž cartesian

  test-Ξ· : βˆ€ {X Y Z} β†’ (f : Hom X (Y βŠ—β‚€ Z))
           β†’ f ≑ ⟨ π₁ ∘ f , Ο€β‚‚ ∘ f ⟩
  test-Ξ· f = products! cartesian

  test-β₁ : βˆ€ {X Y Z} β†’ (f : Hom X Y) β†’ (g : Hom X Z)
            β†’ π₁ ∘ ⟨ f , g ⟩ ≑ f
  test-β₁ f g = products! cartesian

  test-Ξ²β‚‚ : βˆ€ {X Y Z} β†’ (f : Hom X Y) β†’ (g : Hom X Z)
            β†’ Ο€β‚‚ ∘ ⟨ f , g ⟩ ≑ g
  test-Ξ²β‚‚ f g = products! cartesian

  test-⟨⟩∘ : βˆ€ {W X Y Z} β†’ (f : Hom X Y) β†’ (g : Hom X Z) β†’ (h : Hom W X)
             β†’ ⟨ f ∘ h , g ∘ h ⟩ ≑ ⟨ f , g ⟩ ∘ h
  test-⟨⟩∘ f g h = products! cartesian

  -- If you don't have 'withReconstructed' on, this test will fail!
  test-nested : βˆ€ {W X Y Z} β†’ (f : Hom W X) β†’ (g : Hom W Y) β†’ (h : Hom W Z)
             β†’ ⟨ ⟨ f , g ⟩ , h ⟩ ≑ ⟨ ⟨ f , g ⟩ , h ⟩
  test-nested {W} {X} {Y} {Z} f g h = products! cartesian

  test-big : βˆ€ {W X Y Z} β†’ (f : Hom (W βŠ—β‚€ X) (W βŠ—β‚€ Y)) β†’ (g : Hom (W βŠ—β‚€ X) Z)
             β†’ (π₁ ∘ ⟨ f , g ⟩) ∘ id ≑ id ∘ ⟨ π₁ , Ο€β‚‚ ⟩ ∘ f
  test-big f g = products! cartesian

  1. In our context, an Ξ·-law is something like ⟨ π₁ ∘ f , Ο€β‚‚ ∘ f ⟩ ≑ f, where we have an introduction form wrapping a bunch of eliminators applied to the same expression.β†©οΈŽ