diff --git a/src/models/ModelInterface.jl b/src/models/ModelInterface.jl
index 075b3145..682379ed 100644
--- a/src/models/ModelInterface.jl
+++ b/src/models/ModelInterface.jl
@@ -1,6 +1,7 @@
 module ModelInterface
 
-export Model, implements, TypeCheckFail, SignatureMismatchError, @model, @instance, @withmodel, @fail
+export Model, implements, TypeCheckFail, SignatureMismatchError, 
+       @model, @instance, @withmodel, @fail, @migrate
 
 using ...Syntax
 using ...Util.MetaUtils
@@ -8,7 +9,6 @@ using ...Util.MetaUtils
 using MLStyle
 using DataStructures: DefaultDict
 
-
 """
 `Model{Tup <: Tuple}`
 
@@ -134,15 +134,15 @@ macro instance(head, model, body)
   # Parse the head of @instance to get theory and instance types
   (theory_module, instance_types) = @match head begin
     :($ThX{$(Ts...)}) => (ThX, Ts)
+    :($ThX) => (ThX, nothing)
     _ => error("invalid syntax for head of @instance macro: $head")
   end
 
-
   # Get the underlying theory
   theory = macroexpand(__module__, :($theory_module.@theory))
 
   # A dictionary to look up the Julia type of a type constructor from its name (an ident)
-  jltype_by_sort = Dict(zip(sorts(theory), instance_types)) # for type checking
+  jltype_by_sort = isnothing(instance_types) ? nothing : Dict(zip(sorts(theory), instance_types)) # for type checking
 
   # Get the model type that we are overloading for, or nothing if this is the
   # default instance for `instance_types`
@@ -155,9 +155,12 @@ macro instance(head, model, body)
   # Checks that all the functions are defined with the correct types Add default
   # methods for type constructors and type argument accessors if these methods
   # are missing
-  typechecked_functions =
-    typecheck_instance(theory, functions, ext_functions, jltype_by_sort; oldinstance)
-
+  typechecked_functions = if !isnothing(jltype_by_sort) 
+    typecheck_instance(theory, functions, ext_functions, jltype_by_sort; 
+                       oldinstance)
+  else 
+    [functions..., ext_functions...] # skip typechecking and expand_fail
+  end
   # Adds keyword arguments to the functions, and qualifies them by
   # `theory_module`, i.e. changes `Ob(x) = blah` to `ThCategory.Ob(x; model::M,
   # context=nothing) = blah`
@@ -248,6 +251,9 @@ function default_accessor_impl(
   )
 end
 
+julia_signature(theory::GAT, x::Ident, jltype_by_sort::Dict{AlgSort}) = 
+  julia_signature(theory, x, getvalue(theory[x]), jltype_by_sort)
+
 function julia_signature(
   theory::GAT,
   x::Ident,
@@ -382,7 +388,7 @@ function typecheck_instance(
         throw(SignatureMismatchError(f.name, toexpr(sig), expected_signatures[f.name]))
       end
 
-      push!(typechecked, expand_fail(judgment, theory, x, f))
+      push!(typechecked, expand_fail(theory, x, f))
     else
       x = undefined_signatures[sig]
 
@@ -390,7 +396,7 @@ function typecheck_instance(
         judgment = getvalue(theory, x)
 
         if judgment isa AlgTypeConstructor
-          f = expand_fail(judgment, theory, x, f)
+          f = expand_fail(theory, x, f)
         end
       end
 
@@ -417,7 +423,7 @@ function typecheck_instance(
   typechecked
 end
 
-function expand_fail(typecon::AlgTypeConstructor, theory::GAT, x::Ident, f::JuliaFunction)
+function expand_fail(theory::GAT, x::Ident, f::JuliaFunction)
   argname(arg::Expr) = first(arg.args)
   setimpl(
     f,
@@ -504,4 +510,141 @@ macro withmodel(model, subsexpr, body)
   )
 end
 
+
+"""
+Given a Theory Morphism T->U and a type Mᵤ (whose values are models of U), 
+obtain a type Mₜ which has one parameter (of type Mᵤ) and is a model of T.
+
+E.g. given NatIsMonoid: ThMonoid->ThNatPlus and IntPlus <: Model{Tuple{Int}}
+and IntPlus implements ThNatPlus:
+
+```
+@migrate IntPlusMonoid = NatIsMonoid(IntPlus){Int}
+```
+
+Yields:
+
+```
+struct IntPlusMonoid <: Model{Tuple{Int}}
+  model::IntPlus
 end
+
+@instance ThMonoid{Int} [model::IntPlusMonoid] begin ... end 
+```
+
+Future work: There is some subtlety in how accessor functions should be handled.
+TODO: The new instance methods do not yet handle the `context` keyword argument.
+"""
+macro migrate(head)
+  # Parse
+  (name, mapname, modelname) = @match head begin
+    Expr(:(=), name, Expr(:call, mapname, modelname)) => 
+      (name, mapname, modelname)
+    _ => error("could not parse head of @theory: $head")
+  end
+  codom_types = :(only(supertype($(esc(modelname))).parameters).types)
+  # Unpack
+  tmap = macroexpand(__module__, :($mapname.@map))
+  dom_module = macroexpand(__module__, :($mapname.@dom))
+  codom_module = macroexpand(__module__, :($mapname.@codom))
+  dom_theory, codom_theory = TheoryMaps.dom(tmap), TheoryMaps.codom(tmap)
+
+  codom_jltype_by_sort = Dict{Ident,Expr0}(map(enumerate(sorts(codom_theory))) do (i,v) 
+    v.ref => Expr(:ref, codom_types, i)
+  end)
+  _x = gensym("val")
+
+  dom_types = map(sorts(dom_theory)) do s 
+    codom_jltype_by_sort[typemap(tmap)[s.ref].trm.head]
+  end
+  jltype_by_sort = Dict(zip(sorts(dom_theory), dom_types))
+
+  # TypeCons for @instance macro
+  funs = map(collect(typemap(tmap))) do (x, fx)
+    xname = nameof(x)
+    fxname = nameof(fx.trm.head)
+    tc = getvalue(dom_theory[x])
+    jltype_by_sort[AlgSort(fx.trm.head)] = jltype_by_sort[AlgSort(x)]
+    sig = julia_signature(dom_theory, x, jltype_by_sort)
+
+    argnames = [_x, nameof.(argsof(tc))...]
+    args = [:($k::$v) for (k, v) in zip(argnames, sig.types)]
+
+    impls = to_call_impl.(fx.trm.args, Ref(termcons(codom_theory)), Ref(codom_module))
+    impl = Expr(:call, Expr(:ref, :($codom_module.$fxname), :(model.model)), _x, impls...)
+    JuliaFunction(;name=xname, args=args, return_type=sig.types[1], impl=impl)
+  end
+
+  # TermCons for @instance macro
+  funs2 = map(collect(termmap(tmap))) do (x, fx)
+    tc = getvalue(dom_theory[x])
+
+    sig = julia_signature(dom_theory, x, jltype_by_sort)
+    argnames = nameof.(argsof(tc))
+    ret_type = jltype_by_sort[AlgSort(typemap(tmap)[tc.type.head].trm.head)]
+
+    args = [:($k::$v) for (k, v) in zip(argnames, sig.types)]
+
+    impl = to_call_impl(fx.trm, termcons(codom_theory), codom_module)
+
+    JuliaFunction(;name=nameof(x), args=args, return_type=ret_type, impl=impl)
+  end
+
+  funs3 = [] # accessors
+  for (x, fx) in pairs(typemap(tmap))
+    tc = getvalue(dom_theory[x])
+    eq = equations(codom_theory, fx)
+    args = [:($_x::$(jltype_by_sort[AlgSort(fx.trm.head)]))]
+    scopedict = Dict{ScopeTag,ScopeTag}(gettag(tc.localcontext)=>gettag(fx.ctx))
+    for accessor in idents(tc.localcontext; lid=tc.args)
+      accessor = retag(scopedict, accessor)
+      a = nameof(accessor)
+      # If we have a default means of computing the accessor...
+      if !isempty(eq[accessor])
+        rtype = tc.localcontext[ident(tc.localcontext; name=a)]
+        ret_type = jltype_by_sort[AlgSort(getvalue(rtype))]
+        impl = to_call_impl(first(eq[accessor]), _x, codom_module)
+        jf = JuliaFunction(;name=a, args=args, return_type=ret_type, impl=impl)
+        push!(funs3, jf)
+      end
+    end
+  end
+
+  model_expr = Expr(
+    :curly, 
+    GlobalRef(Syntax.TheoryInterface, :Model), 
+    Expr(:curly, :Tuple, dom_types...)
+  )
+
+  quote
+    struct $(esc(name)) <: $model_expr
+      model :: $(esc(modelname))
+    end
+
+    @instance $dom_module [model :: $(esc(name))] begin
+      $(generate_function.([funs...,funs2..., funs3...])...)
+    end
+  end
+end
+
+"""
+Compile an AlgTerm into a Julia call Expr where termcons (e.g. `f`) are 
+interpreted as `mod.f[model.model](...)`.
+"""
+function to_call_impl(t::AlgTerm, termcons, mod::Module)
+  args = to_call_impl.(t.args, Ref(termcons), Ref(mod))
+  name = nameof(headof(t))
+  if t.head in termcons
+    Expr(:call, Expr(:ref, :($mod.$name), :(model.model)), args...)
+  else
+    isempty(args) || error("Bad term $t (termcons=$termcons)")
+    name
+  end
+end
+
+function to_call_impl(t::GATs.AccessorApplication, x::Symbol, mod::Module)
+  rest = t.to isa Ident ? x : to_call_impl(t.to, x, mod)
+  Expr(:call, Expr(:ref, :($mod.$(nameof(t.accessor))), :(model.model)), rest)
+end
+
+end # module
diff --git a/src/stdlib/derivedmodels/DerivedModels.jl b/src/stdlib/derivedmodels/DerivedModels.jl
new file mode 100644
index 00000000..7f8685ba
--- /dev/null
+++ b/src/stdlib/derivedmodels/DerivedModels.jl
@@ -0,0 +1,17 @@
+module DerivedModels
+export OpFinSetC, IntMonoid, IntPreorderCat
+
+using ....Models
+using ...StdTheoryMaps
+using ...StdModels
+
+# Given a model of a category C, we can derive a model of Cᵒᵖ.
+@migrate OpFinSetC = OpCat(FinSetC)
+
+# Interpret `e` as `0` and `⋅` as `+`.
+@migrate IntMonoid = NatPlusMonoid(IntNatPlus)
+
+# Interpret `id` as reflexivity and `compose` as transitivity.
+@migrate IntPreorderCat = PreorderCat(IntPreorder)
+
+end
diff --git a/src/stdlib/derivedmodels/module.jl b/src/stdlib/derivedmodels/module.jl
new file mode 100644
index 00000000..ff474dbd
--- /dev/null
+++ b/src/stdlib/derivedmodels/module.jl
@@ -0,0 +1,9 @@
+module StdDerivedModels
+
+using Reexport
+
+include("DerivedModels.jl") # split into files when big enough
+
+@reexport using .DerivedModels
+
+end
diff --git a/src/stdlib/models/Arithmetic.jl b/src/stdlib/models/Arithmetic.jl
index fd29e5e8..f706cf81 100644
--- a/src/stdlib/models/Arithmetic.jl
+++ b/src/stdlib/models/Arithmetic.jl
@@ -1,6 +1,6 @@
 module Arithmetic 
 
-export IntNatPlus
+export IntNatPlus, IntPreorder
 
 using ....Models
 using ...StdTheories
@@ -13,4 +13,17 @@ struct IntNatPlus <: Model{Tuple{Int}} end
   +(x::Int, y::Int) = x + y
 end
 
+struct IntPreorder <: Model{Tuple{Int, Tuple{Int,Int}}} end
+
+@instance ThPreorder{Int, Tuple{Int,Int}} [model::IntPreorder] begin
+  Leq(ab::Tuple{Int,Int}, a::Int, b::Int) = a ≤ b ? ab : @fail "$(ab[1]) ≰ $(ab[2])"
+  refl(i::Int) = (i, i)
+  trans(ab::Tuple{Int,Int}, bc::Tuple{Int,Int}) = if ab[2] == bc[1] 
+    (ab[1], bc[2])
+  else 
+    error("Cannot compose $ab and $bc")
+  end
+end
+
+
 end # module 
diff --git a/src/stdlib/models/Op.jl b/src/stdlib/models/Op.jl
index cbb6da38..8df58c94 100644
--- a/src/stdlib/models/Op.jl
+++ b/src/stdlib/models/Op.jl
@@ -1,3 +1,7 @@
+"""
+Explicit Op model. Alternatively, see DerivedModels.jl (`OpFinSetC`) for 
+theory-morphism-derived Op models.
+"""
 module Op 
 
 export OpC, op
@@ -7,7 +11,6 @@ using ....Models
 using ...StdTheories
 using StructEquality
 
-
 @struct_hash_equal struct OpC{ObT, HomT, C<:Model{Tuple{ObT, HomT}}} <: Model{Tuple{ObT, HomT}}
   cat::C
 end
diff --git a/src/stdlib/models/module.jl b/src/stdlib/models/module.jl
index dd69e9e0..569fb3ed 100644
--- a/src/stdlib/models/module.jl
+++ b/src/stdlib/models/module.jl
@@ -8,7 +8,7 @@ include("FinMatrices.jl")
 include("SliceCategories.jl")
 include("Op.jl")
 include("Nothings.jl")
-# include("GATs.jl")
+include("GATs.jl")
 
 @reexport using .FinSets
 @reexport using .Arithmetic
@@ -16,6 +16,6 @@ include("Nothings.jl")
 @reexport using .SliceCategories
 @reexport using .Op
 @reexport using .Nothings
-# @reexport using .GATs
+@reexport using .GATs
 
 end
diff --git a/src/stdlib/module.jl b/src/stdlib/module.jl
index af2e079a..742306b3 100644
--- a/src/stdlib/module.jl
+++ b/src/stdlib/module.jl
@@ -4,10 +4,12 @@ using Reexport
 
 include("theories/module.jl")
 include("models/module.jl")
-# include("theorymaps/module.jl")
+include("theorymaps/module.jl")
+include("derivedmodels/module.jl")
 
 @reexport using .StdTheories
 @reexport using .StdModels
-# @reexport using .StdTheoryMaps
+@reexport using .StdTheoryMaps
+@reexport using .StdDerivedModels
 
 end
diff --git a/src/stdlib/theories/Algebra.jl b/src/stdlib/theories/Algebra.jl
index 0a72764d..330b24d0 100644
--- a/src/stdlib/theories/Algebra.jl
+++ b/src/stdlib/theories/Algebra.jl
@@ -1,9 +1,12 @@
 module Algebra
-export ThSet, ThMagma, ThSemiGroup, ThMonoid, ThGroup, ThCMonoid, ThAb, ThRing,
+export ThEmpty, ThSet, ThMagma, ThSemiGroup, ThMonoid, ThGroup, ThCMonoid, ThAb, ThRing,
   ThCRing, ThRig, ThCRig, ThElementary, ThPreorder
 
 using ....Syntax
 
+@theory ThEmpty begin 
+end
+
 @theory ThSet begin
   default::TYPE
 end
diff --git a/src/stdlib/theorymaps/Maps.jl b/src/stdlib/theorymaps/Maps.jl
index 898c9e22..d7261db9 100644
--- a/src/stdlib/theorymaps/Maps.jl
+++ b/src/stdlib/theorymaps/Maps.jl
@@ -5,22 +5,19 @@ export SwapMonoid, NatPlusMonoid, PreorderCat, OpCat
 using ...StdTheories
 using ....Syntax
 
-using GATlab
 SwapMonoid = @theorymap ThMonoid => ThMonoid begin
   default => default
   x⋅y ⊣ [x, y] => y⋅x
   e => e
 end
 
-
-NatPlusMonoid = @theorymap ThMonoid => ThNatPlus  begin
+@theorymap NatPlusMonoid(ThMonoid, ThNatPlus)  begin
   default => ℕ 
   e => Z
   (x ⋅ y) ⊣ [x, y] => x+y
 end
 
-
-OpCat = @theorymap ThCategory => ThCategory begin
+@theorymap OpCat(ThCategory, ThCategory) begin
   Ob => Ob
   Hom(dom, codom) ⊣ [dom::Ob, codom::Ob] => Hom(codom, dom)
   id(a) ⊣ [a::Ob] => id(a)
@@ -28,7 +25,7 @@ OpCat = @theorymap ThCategory => ThCategory begin
 end
 
 """Preorders are categories"""
-PreorderCat = @theorymap ThCategory => ThPreorder begin
+@theorymap PreorderCat(ThCategory, ThPreorder) begin
   Ob => default
   Hom(dom, codom) ⊣ [dom::Ob, codom::Ob] => Leq(dom, codom)
   compose(f, g) ⊣ [a::Ob, b::Ob, c::Ob, f::(a → b), g::(b → c)] => trans(f, g)
@@ -36,8 +33,8 @@ PreorderCat = @theorymap ThCategory => ThPreorder begin
 end
 
 """Thin categories are isomorphic to preorders"""
-# PreorderThinCat = compose(PreorderCat, Incl(ThCategory, ThThinCategory))
-# ThinCatPreorder = inv(PreorderThinCat)
+# PreorderThinCat = @compose(PreorderCat, Incl(ThCategory, ThThinCategory))
+# ThinCatPreorder = @inv(PreorderThinCat)
 
 
 end # module
diff --git a/src/syntax/GATs.jl b/src/syntax/GATs.jl
index 99af1747..d7ef3a70 100644
--- a/src/syntax/GATs.jl
+++ b/src/syntax/GATs.jl
@@ -495,11 +495,25 @@ function equations(context::TypeCtx, args::AbstractVector{Ident}, theory::GAT; i
   ways_of_computing
 end
 
+function equations(theory::GAT, t::TypeInCtx)
+  tc = getvalue(theory[headof(t.trm)])
+  extended = ScopeList([t.ctx, Scope([Binding{AlgType, Nothing}(nothing, t.trm)])])
+  lastx = last(getidents(extended))
+  accessor_args = zip(idents(tc.localcontext; lid=tc.args), t.trm.args)
+  init = Dict{Ident, InferExpr}(map(accessor_args) do (accessor, arg)
+    hasident(t.ctx, headof(arg)) || error("Case not yet handled")
+    headof(arg) => AccessorApplication(accessor, lastx)
+  end)
+  equations(extended, Ident[], theory; init=init)
+end
+
 """Get equations for a term or type constructor"""
 equations(theory::GAT, x::Ident) = let x = getvalue(theory[x]);
   equations(x, idents(x; lid=x.args),theory) 
 end
 
+
+
 function compile(expr_lookup::Dict{Ident}, term::AlgTerm; theorymodule=nothing)
   if term.head isa Constant
     term.head.value
diff --git a/src/syntax/Scopes.jl b/src/syntax/Scopes.jl
index 9a07efc6..99729ebf 100644
--- a/src/syntax/Scopes.jl
+++ b/src/syntax/Scopes.jl
@@ -408,7 +408,10 @@ function make_name_dict(bindings::AbstractVector{Binding{T, Sig}}) where {T, Sig
   d = Dict{Symbol, Dict{Sig, LID}}()
   for (i, binding) in enumerate(bindings)
     name = nameof(binding)
-    if !(name ∈ keys(d))
+    if isnothing(name) 
+      continue 
+    end
+    if !(name ∈ keys(d) )
       d[name] = Dict{Sig, LID}()
     end
     sig = getsignature(binding)
diff --git a/src/syntax/TheoryInterface.jl b/src/syntax/TheoryInterface.jl
index d2b31bae..0f730a1d 100644
--- a/src/syntax/TheoryInterface.jl
+++ b/src/syntax/TheoryInterface.jl
@@ -77,6 +77,7 @@ macro theory(head, body)
   push!(modulelines, :(const THEORY = $theory))
 
   push!(modulelines, :(macro theory() $theory end))
+  push!(modulelines, :(macro theory_module() @__MODULE__ end))
 
   for name in Set(allnames(newsegment))
     # TODO: also push an automatically generated docstring
diff --git a/src/syntax/TheoryMaps.jl b/src/syntax/TheoryMaps.jl
index 263f16fe..3679ce66 100644
--- a/src/syntax/TheoryMaps.jl
+++ b/src/syntax/TheoryMaps.jl
@@ -5,7 +5,7 @@ export IdTheoryMap, TheoryIncl, AbsTheoryMap, TheoryMap, @theorymap,
 using ..GATs, ..Scopes, ..ExprInterop
 using ..Scopes: unsafe_pushbinding!
 using ..GATs: InCtx, TrmTyp, bindingexprs, bind_localctx, substitute_term
-
+using ..TheoryInterface
 import ..ExprInterop: toexpr, fromexpr
 
 using StructEquality, MLStyle
@@ -309,14 +309,31 @@ reorder(b::Binding{T, Sig}, tag::ScopeTag, perm::Dict{Int,Int}) where {T,Sig} =
 
 
 macro theorymap(head, body)
-  (domname, codomname) = @match head begin
-    Expr(:call,:(=>), name, parent) => (name, parent)
+  (name, domname, codomname) = @match head begin
+    Expr(:call, name, domname, codomname) => (name, domname, codomname)
     _ => error("could not parse head of @theory: $head")
   end
 
+  dommod = macroexpand(__module__, :($domname.@theory_module))
+  codommod = macroexpand(__module__, :($codomname.@theory_module))
   dom = macroexpand(__module__, :($domname.@theory))
   codom = macroexpand(__module__, :($codomname.@theory))
-  fromexpr(dom, codom, body, TheoryMap)
+  tmap = fromexpr(dom, codom, body, TheoryMap)
+
+  esc(
+    Expr(
+      :toplevel,
+      :(
+        module $name
+          const MAP = $tmap
+          macro map() $tmap end
+          macro dom() $dommod end
+          macro codom() $codommod end
+        end
+      ),
+      :(Core.@__doc__ $(name)),
+    )
+  )
 end
 
 end # module
diff --git a/src/syntax/module.jl b/src/syntax/module.jl
index 10aff645..b5ee07a3 100644
--- a/src/syntax/module.jl
+++ b/src/syntax/module.jl
@@ -7,13 +7,13 @@ include("ExprInterop.jl")
 include("GATs.jl")
 include("Presentations.jl")
 include("TheoryInterface.jl")
-# include("TheoryMaps.jl")
+include("TheoryMaps.jl")
 
 @reexport using .Scopes
 @reexport using .ExprInterop
 @reexport using .GATs
 @reexport using .Presentations
 @reexport using .TheoryInterface
-# @reexport using .TheoryMaps
+@reexport using .TheoryMaps
 
 end
diff --git a/test/stdlib/models/Arithmetic.jl b/test/stdlib/models/Arithmetic.jl
index 81d3d55d..07bb6a39 100644
--- a/test/stdlib/models/Arithmetic.jl
+++ b/test/stdlib/models/Arithmetic.jl
@@ -3,11 +3,44 @@ module TestArithmetic
 using GATlab
 using Test
 
+# Integers as model of naturals
+#------------------------------
 using .ThNatPlus
 
 @withmodel IntNatPlus() (ℕ, Z, S, +) begin
   @test S(S(Z())) + Z() == 2
 end
 
+# IntMonoid = NatPlusMonoid(IntNatPlus)
+#--------------------------------------
+using .ThMonoid
+
+IM = IntMonoid(IntNatPlus())
+@withmodel IM (e) begin
+  @test e() == 0
+  @test (ThMonoid.:(⋅)[IM])(3, 4) == 7
+end
+
+# Integers as preorder
+#---------------------
+using .ThPreorder
+
+@withmodel IntPreorder() (Leq, refl, trans) begin
+  @test trans((1,3), (3,5)) == (1,5)
+  @test_throws TypeCheckFail Leq((5,3), 5, 3)
+  @test refl(2) == (2,2)
+end
+
+# Now using category interface
+
+using .ThCategory
+M = IntPreorderCat(IntPreorder())
+
+@withmodel M (Hom, id, compose) begin
+  @test compose((1,3), (3,5)) == (1,5)
+  @test_throws TypeCheckFail Hom((5,3), 5, 3)
+  @test_throws ErrorException compose((1,2), (3,5))
+  @test id(2) == (2,2)
+end
 
 end # module 
diff --git a/test/stdlib/models/GATs.jl b/test/stdlib/models/GATs.jl
index f753f5d2..510298bc 100644
--- a/test/stdlib/models/GATs.jl
+++ b/test/stdlib/models/GATs.jl
@@ -1,21 +1,23 @@
 module TestGATs
 
 using GATlab, Test
+
 using .ThCategory
 
-@withmodel GATC() (Ob, Hom, id, compose, dom, codom) begin
+# Uh-oh! This segfaults when inside the @withmodel
+expected = @theorymap ThMonoid => ThNatPlus begin
+  default => ℕ
+  x ⋅ y ⊣ [x, y] => y + x
+  e => Z
+end
 
-  codom(SwapMonoid) == dom(NatPlusMonoid)
+@withmodel GATC() (Ob, Hom, id, compose, dom, codom) begin
 
-  x = toexpr(compose(id(ThMonoid.THEORY), compose(SwapMonoid, NatPlusMonoid)))
+  codom(SwapMonoid.MAP) == dom(NatPlusMonoid.MAP)
 
-  expected = @theorymap ThMonoid => ThNatPlus begin
-    default => ℕ
-    x ⋅ y ⊣ [x, y] => y + x
-    e => Z
-  end
+  x = toexpr(compose(id(ThMonoid.THEORY), compose(SwapMonoid.MAP, NatPlusMonoid.MAP)))
 
-  @test x == toexpr(expected)
+  @test x == toexpr(expected.MAP)
 
 end
 
diff --git a/test/stdlib/models/Op.jl b/test/stdlib/models/Op.jl
index 06295f1f..01882147 100644
--- a/test/stdlib/models/Op.jl
+++ b/test/stdlib/models/Op.jl
@@ -5,6 +5,9 @@ using GATlab, Test
 
 using .ThCategory
 
+# Explicit Op model
+#------------------
+
 @withmodel op(FinSetC()) (Ob, Hom, id, compose, dom, codom) begin
   @test Ob(0) == 0
   @test_throws TypeCheckFail Ob(-1)
@@ -18,4 +21,20 @@ using .ThCategory
   @test dom([5]; context=(dom=10,)) == 10
 end
 
+# Theory-morphism Op
+#-------------------
+
+M = OpFinSetC(FinSetC())
+@withmodel M (Ob, Hom, id, compose, dom, codom) begin
+  @test Ob(0) == 0
+  @test_throws TypeCheckFail Ob(-1)
+  @test_throws TypeCheckFail Hom([1,5,2], 4, 3)
+  @test Hom(Int[], 4, 0) == Int[]
+
+  @test id(2) == [1,2]
+  @test compose([1,1,1,3,2], [5]) == [2]
+  @test codom([5]) == 1
+end
+
+
 end # module
diff --git a/test/stdlib/models/tests.jl b/test/stdlib/models/tests.jl
index 06d4e3ac..7893f362 100644
--- a/test/stdlib/models/tests.jl
+++ b/test/stdlib/models/tests.jl
@@ -6,6 +6,6 @@ include("FinMatrices.jl")
 include("SliceCategories.jl")
 include("Op.jl")
 include("Nothings.jl")
-# include("GATs.jl")
+include("GATs.jl")
 
 end
diff --git a/test/syntax/GATs.jl b/test/syntax/GATs.jl
index 31c67d10..9045f2bf 100644
--- a/test/syntax/GATs.jl
+++ b/test/syntax/GATs.jl
@@ -49,10 +49,9 @@ seg_expr = quote
   ]
 end
 
-
 seg = fromexpr(TypeScope(), seg_expr, GATSegment)
 
-seg[ident(seg;name=:compose, isunique=true)].value.args
+O, H, i, cmp = idents(seg; lid=LID.(1:4))
 
 @test toexpr(TypeScope(), seg) == seg_expr
 
diff --git a/test/syntax/TheoryMaps.jl b/test/syntax/TheoryMaps.jl
index 12e90563..3dc2ed99 100644
--- a/test/syntax/TheoryMaps.jl
+++ b/test/syntax/TheoryMaps.jl
@@ -7,18 +7,23 @@ using Test
 ########
 
 T = ThCategory.THEORY
-T2 = ThPreorder.THEORY
+TP = ThPreorder.THEORY
+TLC = ThLawlessCat.THEORY
+TM = ThMonoid.THEORY
+TNP = ThNatPlus.THEORY
 
+PC = PreorderCat.MAP
+NP = NatPlusMonoid.MAP
 # TheoryMaps 
 ############
-x = toexpr(PreorderCat)
-tm2 = fromexpr(T, T2, x, TheoryMap)
+x = toexpr(PC)
+tm2 = fromexpr(T, TP, x, TheoryMap)
 x2 = toexpr(tm2)
 @test x == x2
 
 # Validation of putative theory maps 
 #-----------------------------------
-@test_throws LoadError @eval @theorymap ThCategory => ThPreorder begin
+@test_throws LoadError @eval @theorymap F(ThCategory, ThPreorder) begin
   Ob => default
   Hom => Leq
   compose(f, g) ⊣ [(a,b,c,d)::Ob, f::(a → b), g::(c → d)] => 
@@ -26,7 +31,7 @@ x2 = toexpr(tm2)
   id(a) ⊣ [a::Ob] => refl(a) ⊣ [a]
 end
 
-@test_throws LoadError @eval @theorymap ThCategory => ThPreorder begin
+@test_throws LoadError @eval @theorymap F(ThCategory, ThPreorder) begin
   Ob => default
   Hom => Leq
   compose(f, g) ⊣ [(a,b,c)::Ob, f::(a → b), g::(b → c)] => 
@@ -42,7 +47,7 @@ end
   id(a) ⊣ [a::Ob] => refl(a) ⊣ [a]
 end
 
-@test_throws LoadError @eval @theorymap ThCategory => ThPreorder begin
+@test_throws LoadError @eval @theorymap F(ThCategory, ThPreorder) begin
   Ob => default
   Hom => Leq
   compose(f, g) ⊣ [a::Ob, b::Ob, c::Ob, f::(a → b), g::(b → c)] => 
@@ -56,43 +61,42 @@ end
 # Test PreorderCat
 
 (Ob, Hom), (Cmp, Id) = typecons(T), termcons(T)
-@test PreorderCat(Ob).trm == AlgType(ident(T2; name=:default))
-@test PreorderCat(Cmp) isa TermInCtx
+@test PC(Ob).trm == AlgType(ident(TP; name=:default))
+@test PC(Cmp) isa TermInCtx
 
-@test PreorderCat(getvalue(T[Cmp]).localcontext) isa TypeScope
+@test PC(getvalue(T[Cmp]).localcontext) isa TypeScope
 
-@test_throws KeyError PreorderCat(first(typecons(T2)))
+@test_throws KeyError PC(first(typecons(TP)))
 
-xterm = fromexpr(ThMonoid.THEORY, :(x ⊣ [x]), TermInCtx)
-res = NatPlusMonoid(xterm)
+xterm = fromexpr(TM, :(x ⊣ [x]), TermInCtx)
+res = NP(xterm)
 toexpr(ThNat.THEORY, res)
 
-xterm = fromexpr(ThMonoid.THEORY, :(e⋅(e⋅x) ⊣ [x]), TermInCtx)
-res = NatPlusMonoid(xterm)
-expected = fromexpr(ThNatPlus.THEORY, :(Z+(Z+x) ⊣ [x::ℕ]), TermInCtx)
-@test toexpr(ThNatPlus.THEORY, res) == toexpr(ThNatPlus.THEORY, expected)
+xterm = fromexpr(TM, :(e⋅(e⋅x) ⊣ [x]), TermInCtx)
+res = NP(xterm)
+expected = fromexpr(TNP, :(Z+(Z+x) ⊣ [x::ℕ]), TermInCtx)
+@test toexpr(TNP, res) == toexpr(TNP, expected)
 
 # Test OpCat
 
 xterm = fromexpr(T, :(id(x) ⋅ p ⋅ q ⋅ id(z) ⊣ [(x,y,z)::Ob, p::Hom(x,y), q::Hom(y,z)]), TermInCtx)
 expected = :(compose(id(z), compose(q,  compose(p, id(x)))) ⊣ [x::Ob,y::Ob,z::Ob, p::Hom(y,x), q::Hom(z,y)])
-@test toexpr(T, OpCat(xterm)) == expected
+@test toexpr(T, OpCat.MAP(xterm)) == expected
 
 
 # Check that maps are not sensitive to order of bindings
 
-OpCat2 = @theorymap ThCategory => ThCategory begin
+@theorymap OpCat2(ThCategory, ThCategory) begin
   Ob => Ob
   Hom(foo, bar) ⊣ [foo::Ob, bar::Ob] => Hom(bar, foo)
   id(a) ⊣ [a::Ob] => id(a)
   compose(p,q) ⊣ [(z,y,x)::Ob, q::Hom(y,z), p::Hom(x,y)] => compose(q, p)
 end
-toexpr(T, OpCat2(xterm)) == expected
+@test toexpr(T, OpCat2.MAP(xterm)) == expected
 
 
 # Inclusions 
 #############
-TLC = ThLawlessCat.THEORY
 incl = TheoryIncl(TLC, T)
 @test TheoryMaps.dom(incl) == TLC
 @test TheoryMaps.codom(incl) == T
diff --git a/test/syntax/tests.jl b/test/syntax/tests.jl
index 6918ba32..47033529 100644
--- a/test/syntax/tests.jl
+++ b/test/syntax/tests.jl
@@ -23,9 +23,9 @@ end
   include("TheoryInterface.jl")
 end
 
-# @testset "TheoryMaps" begin
-#   include("TheoryMaps.jl")
-# end
+@testset "TheoryMaps" begin
+  include("TheoryMaps.jl")
+end
 
 
 end