module Cat.Diagram.Product.Solver where

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

open import 1Lab.Reflection

open import Data.List


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
-- This Ξ·-expands everything, which could make life difficult for agda.
-- Instead, what we want to do is perform type-directe

open Cat.Reasoning π
open Cartesian π 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 (vhom id))


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.

  reflect-hom : β X Y β (f : Hom β¦ X β§β β¦ Y β§β) β reflect X Y (vhom f) β‘ f
reflect-hom X (Y βΆββΆ Z) f =
β¨ reflect X Y (vhom (Οβ β f)) , reflect X Z (vhom (Οβ β f)) β© β‘β¨ apβ β¨_,_β© (reflect-hom X Y (Οβ β f)) (reflect-hom X Z (Οβ β f)) β©β‘
f                                                             β
reflect-hom 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))       β‘β¨ reflect-hom X Y (Οβ β f) β©β‘
Οβ β f                            β‘Λβ¨ reflβ©ββ¨ reflect-hom X (Y βΆββΆ Z) f β©β‘Λ
Οβ β reflect X (Y βΆββΆ Z) (vhom f) β
vfst-sound X Y Z (vpair v1 v2) =
Οβ β β¨ (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))       β‘β¨ reflect-hom X Z (Οβ β f) β©β‘
Οβ β f                            β‘Λβ¨ reflβ©ββ¨ reflect-hom X (Y βΆββΆ Z) f β©β‘Λ
Οβ β reflect X (Y βΆββΆ Z) (vhom f) β
vsnd-sound X Y Z (vpair v1 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.

  reflect-eval : β X Y Z β (e : Expr Y Z) β (v : Value X Y) β reflect X Z (eval e v) β‘ nf Y Z e β reflect X Y v
reflect-eval X Y Y βΆidβΆ v =
reflect X Y v                   β‘β¨ introl (reflect-hom Y Y id) β©β‘
reflect Y Y vid β reflect X Y v β
reflect-eval X Y Z (e1 βΆββΆ e2) v =
reflect X Z (eval e1 (eval e2 v))                   β‘β¨ reflect-eval X _ Z e1 (eval e2 v) β©β‘
nf _ Z e1 β reflect X _ (eval e2 v)                 β‘β¨ reflβ©ββ¨ reflect-eval X Y _ e2 v β©β‘
nf _ Z e1 β nf Y _ e2 β reflect X Y v               β‘β¨ pulll (sym (reflect-eval Y _ Z e1 (eval e2 vid))) β©β‘
reflect Y Z (eval e1 (eval e2 vid)) β reflect X Y v β
reflect-eval X (Y βΆββΆ Z) Y βΆΟββΆ v =
reflect X Y (vfst v)                                         β‘β¨ vfst-sound X Y Z v β©β‘
Οβ β reflect X (Y βΆββΆ Z) v                                   β‘Λβ¨ idr Οβ β©ββ¨refl β©β‘Λ
(Οβ β id) β reflect X (Y βΆββΆ Z) v                            β‘Λβ¨ reflect-hom (Y βΆββΆ Z) Y (Οβ β id) β©ββ¨refl β©β‘Λ
reflect (Y βΆββΆ Z) Y (vhom (Οβ β id)) β reflect X (Y βΆββΆ Z) v β
reflect-eval X (Y βΆββΆ Z) Z βΆΟββΆ v =
reflect X Z (vsnd v)                                         β‘β¨ vsnd-sound X Y Z v β©β‘
Οβ β reflect X (Y βΆββΆ Z) v                                   β‘Λβ¨ idr Οβ β©ββ¨refl β©β‘Λ
(Οβ β id) β reflect X (Y βΆββΆ Z) v                            β‘Λβ¨ reflect-hom (Y βΆββΆ Z) Z (Οβ β id) β©ββ¨refl β©β‘Λ
reflect (Y βΆββΆ Z) Z (vhom (Οβ β id)) β reflect X (Y βΆββΆ Z) v β
reflect-eval X Y (W βΆββΆ Z) βΆβ¨ e1 , e2 β©βΆβΆ v =
β¨ (reflect X W (eval e1 v)) , (reflect X Z (eval e2 v)) β© β‘β¨ apβ β¨_,_β© (reflect-eval X Y W e1 v) (reflect-eval X Y Z e2 v) β©β‘
β¨ nf Y W e1 β reflect X Y v , nf Y Z e2 β reflect X Y v β© β‘Λβ¨ β¨β©β (reflect X Y v) β©β‘Λ
β¨ nf Y W e1 , nf Y Z e2 β© β reflect X Y v                 β
reflect-eval X Y Z βΆ f βΆ v =
reflect X Z (vhom (f β reflect X Y v))                   β‘β¨ reflect-hom X Z (f β reflect X Y v) β©β‘
f β (reflect X Y v)                                      β‘β¨ intror (reflect-hom Y Y id) β©ββ¨refl β©β‘
(f β reflect Y Y vid) β reflect X Y v                    β‘Λβ¨ reflect-hom Y Z (f β reflect Y Y vid) β©ββ¨refl  β©β‘Λ
reflect Y Z (vhom (f β reflect Y Y vid)) β reflect X Y v β


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 X βΆidβΆ = reflect-hom X X id
sound X Z (e1 βΆββΆ e2) =
reflect X Z (eval e1 (eval e2 (vhom id))) β‘β¨ reflect-eval X _ Z e1 (eval e2 (vhom id)) β©β‘
nf _ Z e1 β nf X _ e2                     β‘β¨ apβ _β_ (sound _ Z e1) (sound X  _ e2) β©β‘
β¦ e1 β§β β β¦ e2 β§β                         β
sound (X βΆββΆ Y) X βΆΟββΆ =
nf (X βΆββΆ Y) X βΆΟββΆ β‘β¨ reflect-hom (X βΆββΆ Y) X (Οβ β id) β©β‘
Οβ β id             β‘β¨ idr Οβ β©β‘
Οβ                  β
sound (X βΆββΆ Y) Y βΆΟββΆ =
nf (X βΆββΆ Y) Y βΆΟββΆ β‘β¨ reflect-hom (X βΆββΆ Y) Y (Οβ β id) β©β‘
Οβ β id             β‘β¨ idr Οβ β©β‘
Οβ                  β
sound X (Y βΆββΆ Z) βΆβ¨ e1 , e2 β©βΆβΆ =
β¨ nf X Y e1 , nf X Z e2 β© β‘β¨ apβ β¨_,_β© (sound X Y e1) (sound X Z e2) β©β‘
β¨ β¦ e1 β§β , β¦ e2 β§β β©     β
sound X Y βΆ f βΆ =
nf X Y βΆ f βΆ                β‘β¨ reflect-hom X Y (f β reflect X X (vhom (π .Precategory.id))) β©β‘
(f β reflect X X (vhom id)) β‘β¨ elimr (reflect-hom X X id) β©β‘
f β


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 dontReduceDefs, 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.Οβ β·


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 = ((inferType tm >>= normalise) >>= wait-just-a-bit) >>= Ξ» where
(def (quote Precategory.Hom) (category-field (x vβ· y vβ· []))) β
returnTC (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$
withNormalisation false $dontReduceDefs 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$
withNormalisation false $dontReduceDefs 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 $withNormalisation false$
dontReduceDefs 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β)

solve-macro : β {o β} (π : Precategory o β) (cartesian : β X Y β Product π X Y) β Term β TC β€
solve-macro cat cart hole =
noConstraints $withReconstructed$
withNormalisation false $dontReduceDefs dont-reduce$ do
goal β inferType hole >>= reduce
just (lhs , rhs) β get-boundary goal
where nothing β typeError $strErr "Can't determine boundary: " β· termErr goal β· [] (x , y) β get-objects lhs (x' , y') β get-objects rhs unify x x' unify y y' βxβ β build-obj-expr <$> normalise x
βyβ β build-obj-expr <$> normalise y βlhsβ β build-hom-expr <$> normalise lhs
βrhsβ β build-hom-expr <$> normalise rhs βcatβ β quoteTC cat βcartβ β quoteTC cart (unify hole (βsolveβ βcatβ βcartβ βxβ βyβ βlhsβ βrhsβ)) <|> do vlhs β normalise$ (βnfβ βcatβ βcartβ βxβ βyβ βlhsβ)
vrhs β normalise $(βnfβ βcatβ βcartβ βxβ βyβ βrhsβ) typeError$ strErr "Could not equate the following expressions:\n  " β·
termErr lhs β·
strErr "\nAnd\n  " β·
termErr rhs β·
strErr "\nReflected expressions\n  " β·
termErr βlhsβ β·
strErr "\nAnd\n  " β·
termErr βrhsβ β·
strErr "\nComputed normal forms\n  " β·
termErr vlhs β·
strErr "\nAnd\n  " β·
termErr vrhs β· []


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

products! : β {o β}
β (π : Precategory o β) (cartesian : β X Y β Product π X Y)
β Term β TC β€
products! = Reflection.solve-macro


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 Cartesian π 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)

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.β©οΈ