diff --git a/src/models/ModelInterface.jl b/src/models/ModelInterface.jl
index 8d453c5..01bb58f 100644
--- a/src/models/ModelInterface.jl
+++ b/src/models/ModelInterface.jl
@@ -52,9 +52,9 @@ using ...Syntax
 using ...Util.MetaUtils
 using ...Util.MetaUtils: JuliaFunctionSigNoWhere
 
-import ...Syntax.TheoryMaps: migrator 
 using ...Syntax.TheoryMaps: dom, codom
 using ...Syntax.TheoryInterface: GAT_MODULE_LOOKUP, Dispatch
+import ...Syntax.TheoryInterface: implements, impl_type 
 
 using MLStyle
 using DataStructures: DefaultDict, OrderedDict
diff --git a/src/nonstdlib/module.jl b/src/nonstdlib/module.jl
index be91a91..1f620a3 100644
--- a/src/nonstdlib/module.jl
+++ b/src/nonstdlib/module.jl
@@ -4,12 +4,8 @@ using Reexport
 
 include("theories/module.jl")
 include("models/module.jl")
-# include("theorymaps/module.jl")
-# include("derivedmodels/module.jl")
 
 @reexport using .NonStdTheories
 @reexport using .NonStdModels
-# @reexport using .StdTheoryMaps
-# @reexport using .StdDerivedModels
 
 end
diff --git a/src/stdlib/theories/algebra.jl b/src/stdlib/theories/algebra.jl
index 625d3d7..4f39041 100644
--- a/src/stdlib/theories/algebra.jl
+++ b/src/stdlib/theories/algebra.jl
@@ -1,6 +1,9 @@
-export ThEmpty, ThSet, ThMagma, ThSemiGroup, ThMonoid, ThGroup, ThCMonoid, ThAb, ThSemiRing, ThRing, ThCommRing, ThDiffRing, ThBooleanRing, ThDivisionRing, ThCRig, ThElementary, ThPreorder, ThLeftModule, ThRightModule, ThModule, ThCommRModule
+export ThEmpty, ThSet, ThMagma, ThSemiGroup, ThMonoid, ThGroup, ThCMonoid, ThAb, 
+       ThSemiRing, ThRing, ThCommRing, ThDiffRing, ThBooleanRing, ThDivisionRing, 
+       ThCRig, ThElementary, ThPreorder, ThLeftModule, ThRightModule, ThModule, 
+       ThCommRModule
 
-import Base: +, *, zero, one, -
+import Base: +, *, zero, one, -, inv
 
 @theory ThEmpty begin
 end
diff --git a/src/syntax/Scopes.jl b/src/syntax/Scopes.jl
index 16e17c6..810d867 100644
--- a/src/syntax/Scopes.jl
+++ b/src/syntax/Scopes.jl
@@ -849,7 +849,11 @@ hastag(hsl::HasScopeList, t::ScopeTag) =
 hasname(hsl::HasScopeList, name::Symbol) =
   haskey(getscopelist(hsl).namelookup, name)
 
-getidents(hsl::HasScopeList; kw...) = vcat(getidents.(getscopelist(hsl); kw...)...)
+getidents(hsl::HasScopeList; kw...) = 
+  vcat(getidents.(getscopelist(hsl); kw...)...)
+
+identvalues(hsl::HasScopeList) = 
+  vcat(identvalues.(getscopelist(hsl))...)
 
 alltags(hsl::HasScopeList) = Set(gettag.(getscopelist(hsl).scopes))
 
diff --git a/src/syntax/TheoryInterface.jl b/src/syntax/TheoryInterface.jl
index 8fc1d7d..904bfdd 100644
--- a/src/syntax/TheoryInterface.jl
+++ b/src/syntax/TheoryInterface.jl
@@ -1,13 +1,3 @@
-module TheoryInterface
-export @theory, @signature, invoke_term
-
-using ..Scopes, ..GATs, ..ExprInterop, GATlab.Util
-
-using MLStyle, StructEquality, Markdown
-
-@struct_hash_equal struct WithModel{M}
-  model::M
-end
 
 """
 Each theory corresponds to a module, which has the following items.
@@ -29,7 +19,27 @@ For all aliases, `const` declarations that make them equal to their primaries.
 A macro called `@theory` which expands to the `GAT` data structure for the module.
 
 A constant called `Meta.theory` which is the `GAT` data structure.
+
+A struct called `Meta.Wrapper` which is a smart constructor for Julia types 
+which implement the theory.
 """
+module TheoryInterface
+export @theory, @signature, invoke_term, wrapper, ModelWrapper
+
+using ..Scopes, ..GATs, ..ExprInterop, GATlab.Util
+
+using MLStyle, StructEquality, Markdown
+import AlgebraicInterfaces: getvalue
+
+@struct_hash_equal struct WithModel{M}
+  model::M
+end
+
+getvalue(m::WithModel) = m.model
+
+function implements end # implemented in ModelInterface
+
+function impl_type end # implemented in ModelInterface
 
 # TODO is every contribution to a theory a new segment, or can a new theory introduce multiple segments? 
 """
@@ -153,7 +163,7 @@ function theory_impl(head, body, __module__)
   mdp(::Nothing) = []
   mdp(x::Markdown.MD) = x
   mdp(x::Base.Docs.DocStr) = Markdown.parse(x.text...)
-
+  wrapper_expr = wrapper(name, theory, fqmn(__module__))
   push!(modulelines, Expr(:toplevel, :(module Meta
     struct T end
    
@@ -161,6 +171,8 @@ function theory_impl(head, body, __module__)
 
     macro theory() $theory end
     macro theory_module() parentmodule(@__MODULE__) end
+
+    $wrapper_expr
   end)))
 
   # XXX
@@ -175,8 +187,8 @@ function theory_impl(head, body, __module__)
       :(Core.@__doc__ $(doctarget)),
       :(
         module $name
-        $(modulelines...)
         $(structlines...)
+        $(modulelines...)
         end
       ),
       :(@doc ($(Markdown.MD)($mdp(@doc $doctarget), $docstr)) $name)
@@ -250,4 +262,51 @@ function mk_struct(s::AlgStruct, mod)
   end
 end
 
+# Wrapper type 
+##############
+
+
+function wrapper(name::Symbol, t::GAT, mod)
+  use = Expr(:using, Expr(:., :., :., name))
+  quote
+    $use
+    macro wrapper(n)
+      esc(:($($(name)).Meta.@wrapper $n $Any))
+    end
+    macro abs_wrapper(n)
+      n.head == :<: || error("Expected: StructName <: AbsType, got $n")
+      x, y = n.args
+      esc(:($($(name)).Meta.@wrapper $(x) $(y)))
+    end
+    macro wrapper(n, abs)
+      esc(quote 
+        struct $n <: $abs
+          val::Any
+          function $n(x::Any)
+            $($(GlobalRef(TheoryInterface, :implements)))(x, $($name)) || error(
+              "Invalid $($($(name))) model: $x")
+            new(x)
+          end
+        end
+        $(Expr(:macrocall, $(GlobalRef(StructEquality, Symbol("@struct_hash_equal"))), $(mod), $(:n)))
+
+        GATlab.getvalue(x::$n) = x.val # GlobalRef doesn't work: "invalid function name"
+        GATlab.impl_type(x::$n, o::Symbol) = GATlab.impl_type(x.val, $($name), o)
+
+        $(map($(identvalues(t))) do (x,j)
+        if j isa $(AlgDeclaration) 
+          op = nameof(x)
+          :($($(name)).$op(x::$(($(:n))), args...; kw...) = 
+            $($(name)).$op[x.val](args...; kw...))
+        else
+          :()
+        end
+      end...)
+      $n
+      end)
+    end
+  end
 end
+
+
+end # module
diff --git a/src/syntax/TheoryMaps.jl b/src/syntax/TheoryMaps.jl
index 4364dfe..c679b3e 100644
--- a/src/syntax/TheoryMaps.jl
+++ b/src/syntax/TheoryMaps.jl
@@ -418,7 +418,4 @@ macro theorymap(head, body)
   )
 end
 
-function migrator end
-
-
 end # module
diff --git a/test/models/ModelInterface.jl b/test/models/ModelInterface.jl
index 185575e..232dd71 100644
--- a/test/models/ModelInterface.jl
+++ b/test/models/ModelInterface.jl
@@ -229,4 +229,30 @@ d = Dispatch(ThCategory.Meta.theory, [Int, Vector{Int}])
 @test id(2) == [1,2] == ThCategory.id[d](2)
 @test compose([1,2,3], [2,1,3]) == [2,1,3]
  
+# Test wrapper structs
+######################
+ThCategory.Meta.@wrapper Cat
+
+c = Cat(FinSetC());
+c2 = Cat(FinMatC{Int}());
+@test_throws ErrorException Cat(MyVect([1,2,3])) # can't construct
+
+@test getvalue(c) == FinSetC()
+@test impl_type(c, :Ob) == Int == impl_type(c2, :Ob)
+
+@test Ob(c, 2) == 2
+@test_throws MethodError Hom(c2, [1,2])
+
+function id2(c::Cat)
+  ThCategory.id(c, 2)
+end
+
+@test id2(c) == [1,2]
+@test id2(c2) == [1 0; 0 1]
+@test_throws MethodError id2(FinSetC())
+
+abstract type MyAbsType end
+ThCategory.Meta.@abs_wrapper Cat2 <: MyAbsType 
+@test Cat2 <: MyAbsType
+
 end # module