philzook58

using Pkg
Pkg.activate("metatheory")
Pkg.add(url="https://github.com/0x0f0f0f/Metatheory.jl.git")
using Metatheory
using Metatheory.EGraphs

cat_theory = @theory begin
	hom(hom(f, ob(a), ob(b)) ⋅ hom(id(ob(b)), ob(b), ob(b)), ob(a), ob(b)) == hom(f, ob(a), ob(b))
	hom(hom(id(ob(a)), ob(a), ob(a)) ⋅ hom(f, ob(a), ob(b)), ob(a), ob(b)) == hom(f, ob(a), ob(b))
	hom(hom(f, ob(a), ob(b)) ⋅ hom(hom(g, ob(b), ob(c)) ⋅ hom(h, ob(c), ob(d)), ob(b), ob(d)), ob(a), ob(d)) == hom(hom(hom(f, ob(a), ob(b)) ⋅ hom(g, ob(b), ob(c)), ob(a), ob(c)) ⋅ hom(h, ob(c), ob(d)), ob(a), ob(d))