diff --git a/src/syntax/gats/exprinterop.jl b/src/syntax/gats/exprinterop.jl
index 27ac0cb4..4211141d 100644
--- a/src/syntax/gats/exprinterop.jl
+++ b/src/syntax/gats/exprinterop.jl
@@ -67,7 +67,7 @@ function toexpr(c::Context, type::AlgType)
       Expr(:call, toexpr(c, type.body.head), toexpr.(Ref(c), type.body.args)...)
     end
   else
-    Expr(:call, :(==), type.body.equands...)
+    Expr(:call, :(==), toexpr.(Ref(c), type.body.equands)...)
   end
 end
 
@@ -105,8 +105,6 @@ end
 # Judgments
 ###########
 
-# toexpr
-
 function toexpr(p::Context, b::Binding{AlgType})
   val = getvalue(b)
   if isapp(val)
@@ -172,16 +170,6 @@ function toexpr(c::GAT, binding::Binding{Judgment})
   Expr(:call, :(⊣), head, Expr(:vect, bindingexprs(c, judgment.localcontext)...))
 end
 
-function toexpr(c::Context, p::GATContext)
-  c == p.theory || error("Invalid context for presentation")
-  decs = GATs.bindingexprs(c, p.scope)
-  eqs = map(p.eqs) do ts
-    exprs = zip(toexpr.(Ref(p), ts),Iterators.repeated(:(==)))
-    Expr(:comparison, collect(Iterators.flatten(exprs))[1:(end-1)]...)
-  end
-  Expr(:block, [decs..., eqs...]...)
-end
-
 # fromexpr
 
 """
diff --git a/test/syntax/GATContexts.jl b/test/syntax/GATContexts.jl
index 8d56c778..cb0e4bb0 100644
--- a/test/syntax/GATContexts.jl
+++ b/test/syntax/GATContexts.jl
@@ -58,4 +58,6 @@ a = ident(Z; name=:a)
   (r⋅r⋅r⋅r) == e()
 end
 
+@test sprint(show, D₄)[1] == 'G' # etc.
+
 end # module 
diff --git a/test/syntax/GATs.jl b/test/syntax/GATs.jl
index 47e993bb..48e64663 100644
--- a/test/syntax/GATs.jl
+++ b/test/syntax/GATs.jl
@@ -52,6 +52,7 @@ O, H, i, cmp = idents(thcat; name=[:Ob, :Hom, :id, :compose])
 
 ObT = fromexpr(thcat, :Ob, AlgType)
 ObS = AlgSort(ObT)
+@test toexpr(GATContext(thcat), ObS) == :Ob
 
 # Extend seg with a context of (A: Ob)
 sortscope = TypeScope(:A => ObT)
@@ -63,6 +64,11 @@ ATerm = AlgTerm(A)
 c = GATContext(thcat, sortscope)
 
 HomT = fromexpr(c, :(Hom(A, A)), AlgType)
+
+AA = :(A == A)
+eqA = fromexpr(c, AA, AlgType)
+@test toexpr(c, eqA) == AA
+
 HomS = AlgSort(HomT)
 
 @test rename(gettag(sortscope), Dict(:A=>:Z), HomT) isa AlgType
diff --git a/test/syntax/TheoryInterface.jl b/test/syntax/TheoryInterface.jl
index f5eae269..d41f2f34 100644
--- a/test/syntax/TheoryInterface.jl
+++ b/test/syntax/TheoryInterface.jl
@@ -37,6 +37,11 @@ using .ThLawlessCategory
   Hom(dom::Ob, codom::Ob) :: TYPE
 end
 
+@test_throws Exception @eval @theory ThMonoid <: ThSemiGroup begin
+  e() :: default
+  e ⋅ x == x ⊣ [x]
+end
+
 @test_throws Exception @eval @theory ThBadAliases <: ThCategory begin
   @op 1 + 1
 end