diff --git a/src/models/ModelInterface.jl b/src/models/ModelInterface.jl
index 84cf137..b7414ac 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..de69ab4 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,35 @@ 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
+
+""" Parse markdown coming out of @doc programatically. """
+mdp(::Nothing) = ""
+mdp(x::Markdown.MD) = x
+function mdp(x::Base.Docs.DocStr)
+  Markdown.parse(only(x.text))
+end
+
 
 # TODO is every contribution to a theory a new segment, or can a new theory introduce multiple segments? 
 """
@@ -150,10 +168,7 @@ function theory_impl(head, body, __module__)
   end
   
   doctarget = gensym()
-  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 +176,8 @@ function theory_impl(head, body, __module__)
 
     macro theory() $theory end
     macro theory_module() parentmodule(@__MODULE__) end
+
+    $wrapper_expr
   end)))
 
   # XXX
@@ -175,8 +192,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 +267,118 @@ 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)
+      x, y = $(parse_wrapper_input)(n)
+      esc(:($($(name)).Meta.@wrapper $x $y))
+    end
+
+    macro typed_wrapper(n)
+      x, y = $(parse_wrapper_input)(n)
+      esc(:($($(name)).Meta.@typed_wrapper $x $y))
+    end
+
+    macro wrapper(n, abs)
+      doctarget = gensym()
+      esc(quote 
+        # Catch any potential docs above the macro call
+        const $(doctarget) = nothing
+        Core.@__doc__ $(doctarget)
+
+        # Declare the wrapper struct
+        struct $n <: $abs
+          val::Any
+          function $n(x::Any)
+            $($(GlobalRef(TheoryInterface, :implements)))(x, $($name)) || error(
+              "Invalid $($($(name))) model: $x")
+            new(x)
+          end
+        end
+        # Apply the caught documentation to the new struct
+        @doc $($(mdp))(@doc $doctarget) $n
+
+        # Define == and hash
+        $(Expr(:macrocall, $(GlobalRef(StructEquality, Symbol("@struct_hash_equal"))), $(mod), $(:n)))
+
+        # GlobalRef doesn't work: "invalid function name".
+        GATlab.getvalue(x::$n) = x.val 
+        GATlab.impl_type(x::$n, o::Symbol) = GATlab.impl_type(x.val, $($name), o)
+
+        # Dispatch on model value for all declarations in theory
+        $(map(filter(x->x[2] isa $AlgDeclaration, $(identvalues(t)))) do (x,j)
+          if j isa $(AlgDeclaration) 
+            op = nameof(x)
+            :($($(name)).$op(x::$(($(:n))), args...; kw...) = 
+              $($(name)).$op[x.val](args...; kw...))
+          end
+      end...)
+      nothing
+      end)
+    end
+
+    macro typed_wrapper(n, abs)
+      doctarget = gensym()
+      Ts = nameof.($(sorts)($t))
+      Xs = map(Ts) do s 
+        :($(GlobalRef($(TheoryInterface), :impl_type))(x, $($(name)), $($(Meta.quot)(s))))
+      end
+      XTs = map(zip(Ts,Xs)) do (T,X)
+        :($X <: $T || error("Mismatch $($($(Meta.quot)(T))): $($X) ⊄ $($T)"))
+      end
+      esc(quote 
+        # Catch any potential docs above the macro call
+        const $(doctarget) = nothing
+        Core.@__doc__ $(doctarget)
+
+        # Declare the wrapper struct
+        struct $n{$(Ts...)} <: $abs
+          val::Any
+          function $n{$(Ts...)}(x::Any) where {$(Ts...)}
+            $($(GlobalRef(TheoryInterface, :implements)))(x, $($name)) || error(
+              "Invalid $($($(name))) model: $x")
+            $(XTs...)
+            # CHECK THAT THE GIVEN PARAMETERS MATCH Xs
+            new{$(Ts...)}(x)
+          end
+
+          function $n(x::Any)
+            $($(GlobalRef(TheoryInterface, :implements)))(x, $($name)) || error(
+              "Invalid $($($(name))) model: $x")
+            new{$(Xs...)}(x)
+          end
+        end
+        # Apply the caught documentation to the new struct
+        @doc $($(mdp))(@doc $doctarget) $n
+
+        # Define == and hash
+        $(Expr(:macrocall, $(GlobalRef(StructEquality, Symbol("@struct_hash_equal"))), $(mod), $(:n)))
+
+        # GlobalRef doesn't work: "invalid function name".
+        GATlab.getvalue(x::$n) = x.val 
+        GATlab.impl_type(x::$n, o::Symbol) = GATlab.impl_type(x.val, $($name), o)
+
+        # Dispatch on model value for all declarations in theory
+        $(map(filter(x->x[2] isa $AlgDeclaration, $(identvalues(t)))) do (x,j)
+          if j isa $(AlgDeclaration) 
+            op = nameof(x)
+            :($($(name)).$op(x::$(($(:n))), args...; kw...) = 
+              $($(name)).$op[x.val](args...; kw...))
+          end
+      end...)
+      nothing
+      end)
+    end
+  end
 end
+
+parse_wrapper_input(n::Symbol) = n, Any
+parse_wrapper_input(n::Expr) = n.head == :<: ? n.args : error("Bad input for wrapper")
+
+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..3e5e262 100644
--- a/test/models/ModelInterface.jl
+++ b/test/models/ModelInterface.jl
@@ -229,4 +229,47 @@ 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
+######################
+"""Cat"""
+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.@wrapper Cat2 <: MyAbsType 
+@test Cat2 <: MyAbsType
+
+# Typed wrappers
+#----------------
+"""Typed Cat"""
+ThCategory.Meta.@typed_wrapper TCat
+
+c = TCat(FinSetC())
+@test c == TCat{Int,Vector{Int}}(FinSetC())
+@test_throws ErrorException TCat{Bool,Symbol}(FinSetC()) # Ob: Int ⊄ Bool
+@test c isa TCat{Int, Vector{Int}}
+@test id(c, 2) == [1,2]
+
+c2 = TCat(FinMatC{Int}());
+@test c2 isa TCat{Int, Matrix{Int}}
+
+@test id(c2, 2) == [1 0; 0 1]
+
 end # module