type tagged Category theor in metatheory.,jly

cat.jl

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))
	ob(ob(a) ⊗ ob(munit())) == ob(a)
	ob(ob(munit()) ⊗ ob(a)) == ob(a)
	ob(ob(a) ⊗ ob(ob(b) ⊗ ob(c))) == ob(ob(ob(a) ⊗ ob(b)) ⊗ ob(c))
	hom(hom(f, ob(a), ob(b)) ⊗ hom(hom(h, ob(c), ob(d)) ⊗ hom(j, ob(m), ob(n)), ob(ob(c) ⊗ ob(m)), ob(ob(d) ⊗ ob(n))), ob(ob(a) ⊗ ob(ob(c) ⊗ ob(m))), ob(ob(b) ⊗ ob(ob(d) ⊗ ob(n)))) == hom(hom(hom(f, ob(a), ob(b)) ⊗ hom(h, ob(c), ob(d)), ob(ob(a) ⊗ ob(c)), ob(ob(b) ⊗ ob(d))) ⊗ hom(j, ob(m), ob(n)), ob(ob(ob(a) ⊗ ob(c)) ⊗ ob(m)), ob(ob(ob(b) ⊗ ob(d)) ⊗ ob(n)))
	hom(id(ob(ob(a) ⊗ ob(b))), ob(ob(a) ⊗ ob(b)), ob(ob(a) ⊗ ob(b))) == hom(hom(id(ob(a)), ob(a), ob(a)) ⊗ hom(id(ob(b)), ob(b), ob(b)), ob(ob(a) ⊗ ob(b)), ob(ob(a) ⊗ ob(b)))
	hom(hom(hom(f, ob(a), ob(b)) ⊗ hom(p, ob(x), ob(y)), ob(ob(a) ⊗ ob(x)), ob(ob(b) ⊗ ob(y))) ⋅ hom(hom(g, ob(b), ob(c)) ⊗ hom(q, ob(y), ob(z)), ob(ob(b) ⊗ ob(y)), ob(ob(c) ⊗ ob(z))), ob(ob(a) ⊗ ob(x)), ob(ob(c) ⊗ ob(z))) == hom(hom(hom(f, ob(a), ob(b)) ⋅ hom(g, ob(b), ob(c)), ob(a), ob(c)) ⊗ hom(hom(p, ob(x), ob(y)) ⋅ hom(q, ob(y), ob(z)), ob(x), ob(z)), ob(ob(a) ⊗ ob(x)), ob(ob(c) ⊗ ob(z)))
	hom(hom(σ(ob(a), ob(b)), ob(ob(a) ⊗ ob(b)), ob(ob(b) ⊗ ob(a))) ⋅ hom(σ(ob(b), ob(a)), ob(ob(b) ⊗ ob(a)), ob(ob(a) ⊗ ob(b))), ob(ob(a) ⊗ ob(b)), ob(ob(a) ⊗ ob(b))) == hom(id(ob(ob(a) ⊗ ob(b))), ob(ob(a) ⊗ ob(b)), ob(ob(a) ⊗ ob(b)))
	hom(σ(ob(a), ob(ob(b) ⊗ ob(c))), ob(ob(a) ⊗ ob(ob(b) ⊗ ob(c))), ob(ob(ob(b) ⊗ ob(c)) ⊗ ob(a))) == hom(hom(hom(σ(ob(a), ob(b)), ob(ob(a) ⊗ ob(b)), ob(ob(b) ⊗ ob(a))) ⊗ hom(id(ob(c)), ob(c), ob(c)), ob(ob(ob(a) ⊗ ob(b)) ⊗ ob(c)), ob(ob(ob(b) ⊗ ob(a)) ⊗ ob(c))) ⋅ hom(hom(id(ob(b)), ob(b), ob(b)) ⊗ hom(σ(ob(a), ob(c)), ob(ob(a) ⊗ ob(c)), ob(ob(c) ⊗ ob(a))), ob(ob(b) ⊗ ob(ob(a) ⊗ ob(c))), ob(ob(b) ⊗ ob(ob(c) ⊗ ob(a)))), ob(ob(ob(a) ⊗ ob(b)) ⊗ ob(c)), ob(ob(b) ⊗ ob(ob(c) ⊗ ob(a))))
	hom(σ(ob(ob(a) ⊗ ob(b)), ob(c)), ob(ob(ob(a) ⊗ ob(b)) ⊗ ob(c)), ob(ob(c) ⊗ ob(ob(a) ⊗ ob(b)))) == hom(hom(hom(id(ob(a)), ob(a), ob(a)) ⊗ hom(σ(ob(b), ob(c)), ob(ob(b) ⊗ ob(c)), ob(ob(c) ⊗ ob(b))), ob(ob(a) ⊗ ob(ob(b) ⊗ ob(c))), ob(ob(a) ⊗ ob(ob(c) ⊗ ob(b)))) ⋅ hom(hom(σ(ob(a), ob(c)), ob(ob(a) ⊗ ob(c)), ob(ob(c) ⊗ ob(a))) ⊗ hom(id(ob(b)), ob(b), ob(b)), ob(ob(ob(a) ⊗ ob(c)) ⊗ ob(b)), ob(ob(ob(c) ⊗ ob(a)) ⊗ ob(b))), ob(ob(a) ⊗ ob(ob(b) ⊗ ob(c))), ob(ob(ob(c) ⊗ ob(a)) ⊗ ob(b)))
	hom(hom(hom(f, ob(a), ob(b)) ⊗ hom(h, ob(c), ob(d)), ob(ob(a) ⊗ ob(c)), ob(ob(b) ⊗ ob(d))) ⋅ hom(σ(ob(b), ob(d)), ob(ob(b) ⊗ ob(d)), ob(ob(d) ⊗ ob(b))), ob(ob(a) ⊗ ob(c)), ob(ob(d) ⊗ ob(b))) == hom(hom(σ(ob(a), ob(c)), ob(ob(a) ⊗ ob(c)), ob(ob(c) ⊗ ob(a))) ⋅ hom(hom(h, ob(c), ob(d)) ⊗ hom(f, ob(a), ob(b)), ob(ob(c) ⊗ ob(a)), ob(ob(d) ⊗ ob(b))), ob(ob(a) ⊗ ob(c)), ob(ob(d) ⊗ ob(b)))
	hom(hom(Δ(ob(a)), ob(a), ob(ob(a) ⊗ ob(a))) ⋅ hom(hom(Δ(ob(a)), ob(a), ob(ob(a) ⊗ ob(a))) ⊗ hom(id(ob(a)), ob(a), ob(a)), ob(ob(a) ⊗ ob(a)), ob(ob(ob(a) ⊗ ob(a)) ⊗ ob(a))), ob(a), ob(ob(ob(a) ⊗ ob(a)) ⊗ ob(a))) == hom(hom(Δ(ob(a)), ob(a), ob(ob(a) ⊗ ob(a))) ⋅ hom(hom(id(ob(a)), ob(a), ob(a)) ⊗ hom(Δ(ob(a)), ob(a), ob(ob(a) ⊗ ob(a))), ob(ob(a) ⊗ ob(a)), ob(ob(a) ⊗ ob(ob(a) ⊗ ob(a)))), ob(a), ob(ob(a) ⊗ ob(ob(a) ⊗ ob(a))))
	hom(hom(Δ(ob(a)), ob(a), ob(ob(a) ⊗ ob(a))) ⋅ hom(hom((⋄)(ob(a)), ob(a), ob(munit())) ⊗ hom(id(ob(a)), ob(a), ob(a)), ob(ob(a) ⊗ ob(a)), ob(ob(munit()) ⊗ ob(a))), ob(a), ob(ob(munit()) ⊗ ob(a))) == hom(id(ob(a)), ob(a), ob(a))
	hom(hom(Δ(ob(a)), ob(a), ob(ob(a) ⊗ ob(a))) ⋅ hom(hom(id(ob(a)), ob(a), ob(a)) ⊗ hom((⋄)(ob(a)), ob(a), ob(munit())), ob(ob(a) ⊗ ob(a)), ob(ob(a) ⊗ ob(munit()))), ob(a), ob(ob(a) ⊗ ob(munit()))) == hom(id(ob(a)), ob(a), ob(a))
	hom(hom(Δ(ob(a)), ob(a), ob(ob(a) ⊗ ob(a))) ⋅ hom(σ(ob(a), ob(a)), ob(ob(a) ⊗ ob(a)), ob(ob(a) ⊗ ob(a))), ob(a), ob(ob(a) ⊗ ob(a))) == hom(Δ(ob(a)), ob(a), ob(ob(a) ⊗ ob(a)))
	hom(Δ(ob(ob(a) ⊗ ob(b))), ob(ob(a) ⊗ ob(b)), ob(ob(ob(a) ⊗ ob(b)) ⊗ ob(ob(a) ⊗ ob(b)))) == hom(hom(hom(Δ(ob(a)), ob(a), ob(ob(a) ⊗ ob(a))) ⊗ hom(Δ(ob(b)), ob(b), ob(ob(b) ⊗ ob(b))), ob(ob(a) ⊗ ob(b)), ob(ob(ob(a) ⊗ ob(a)) ⊗ ob(ob(b) ⊗ ob(b)))) ⋅ hom(hom(hom(id(ob(a)), ob(a), ob(a)) ⊗ hom(σ(ob(a), ob(b)), ob(ob(a) ⊗ ob(b)), ob(ob(b) ⊗ ob(a))), ob(ob(a) ⊗ ob(ob(a) ⊗ ob(b))), ob(ob(a) ⊗ ob(ob(b) ⊗ ob(a)))) ⊗ hom(id(ob(b)), ob(b), ob(b)), ob(ob(ob(a) ⊗ ob(ob(a) ⊗ ob(b))) ⊗ ob(b)), ob(ob(ob(a) ⊗ ob(ob(b) ⊗ ob(a))) ⊗ ob(b))), ob(ob(a) ⊗ ob(b)), ob(ob(ob(a) ⊗ ob(ob(b) ⊗ ob(a))) ⊗ ob(b)))
	hom((⋄)(ob(ob(a) ⊗ ob(b))), ob(ob(a) ⊗ ob(b)), ob(munit())) == hom(hom((⋄)(ob(a)), ob(a), ob(munit())) ⊗ hom((⋄)(ob(b)), ob(b), ob(munit())), ob(ob(a) ⊗ ob(b)), ob(ob(munit()) ⊗ ob(munit())))
	hom(Δ(ob(munit())), ob(munit()), ob(ob(munit()) ⊗ ob(munit()))) == hom(id(ob(munit())), ob(munit()), ob(munit()))
	hom((⋄)(ob(munit())), ob(munit()), ob(munit())) == hom(id(ob(munit())), ob(munit()), ob(munit()))
	hom(pair(hom(f, ob(a), ob(b)), hom(k, ob(a), ob(c))), ob(a), ob(ob(b) ⊗ ob(c))) == hom(hom(Δ(ob(a)), ob(a), ob(ob(a) ⊗ ob(a))) ⋅ hom(hom(f, ob(a), ob(b)) ⊗ hom(k, ob(a), ob(c)), ob(ob(a) ⊗ ob(a)), ob(ob(b) ⊗ ob(c))), ob(a), ob(ob(b) ⊗ ob(c)))
	hom(proj1(ob(a), ob(b)), ob(ob(a) ⊗ ob(b)), ob(a)) == hom(hom(id(ob(a)), ob(a), ob(a)) ⊗ hom((⋄)(ob(b)), ob(b), ob(munit())), ob(ob(a) ⊗ ob(b)), ob(ob(a) ⊗ ob(munit())))
	hom(hom(id(ob(a)), ob(a), ob(a)) ⊗ hom((⋄)(ob(b)), ob(b), ob(munit())), ob(ob(a) ⊗ ob(b)), ob(ob(a) ⊗ ob(munit()))) == hom(proj1(ob(a), ob(b)), ob(ob(a) ⊗ ob(b)), ob(a))
	hom(proj2(ob(a), ob(b)), ob(ob(a) ⊗ ob(b)), ob(b)) == hom(hom((⋄)(ob(a)), ob(a), ob(munit())) ⊗ hom(id(ob(b)), ob(b), ob(b)), ob(ob(a) ⊗ ob(b)), ob(ob(munit()) ⊗ ob(b)))
	hom(hom(f, ob(a), ob(b)) ⋅ hom(Δ(ob(b)), ob(b), ob(ob(b) ⊗ ob(b))), ob(a), ob(ob(b) ⊗ ob(b))) == hom(hom(Δ(ob(a)), ob(a), ob(ob(a) ⊗ ob(a))) ⋅ hom(hom(f, ob(a), ob(b)) ⊗ hom(f, ob(a), ob(b)), ob(ob(a) ⊗ ob(a)), ob(ob(b) ⊗ ob(b))), ob(a), ob(ob(b) ⊗ ob(b)))
	hom(hom(f, ob(a), ob(b)) ⋅ hom((⋄)(ob(b)), ob(b), ob(munit())), ob(a), ob(munit())) == hom((⋄)(ob(b)), ob(b), ob(munit()))
end

# for pretty printing
function untag( e::Expr )
    if e.args[1] == :hom
        untag(e.args[2])
    elseif(e.args[1] == :ob)
        untag(e.args[2])
    else
        Expr(e.head, [untag(e) for e in e.args]...)
    end
end

untag(e::Symbol) = e

pair_proj1_proj2 = :(hom(pair(hom(proj1(ob(a), ob(b)), ob(ob(a) ⊗ ob(b)), ob(a)), hom(proj2(ob(a), ob(b)), ob(ob(a) ⊗ ob(b)), ob(b))), ob(ob(a) ⊗ ob(b)), ob(ob(a) ⊗ ob(b))))
println(untag(pair_proj1_proj2))
G = EGraph(pair_proj1_proj2)
@time saturate!(G, cat_theory, timeout=1)
extractor = addanalysis!(G, ExtractionAnalysis, astsize)
ex = extract!(G, extractor)
println(untag(ex))