diff --git a/src/models/ModelInterface.jl b/src/models/ModelInterface.jl
index 6d008bab..8d453c57 100644
--- a/src/models/ModelInterface.jl
+++ b/src/models/ModelInterface.jl
@@ -1,25 +1,7 @@
-module ModelInterface
-
-export Model, implements, TypeCheckFail, SignatureMismatchError, 
-       @model, @instance, @withmodel, @fail, migrate_model
-
-using ...Syntax
-using ...Util.MetaUtils
-using ...Util.MetaUtils: JuliaFunctionSigNoWhere
-
-import ...Syntax.TheoryMaps: migrator 
-
-using MLStyle
-using DataStructures: DefaultDict, OrderedDict
 
 """
-`Model{Tup <: Tuple}`
-
-A Julia value with type `Model{Tuple{Ts...}}` represents a model of some
-part of the theory hierarchy, which uses the types in `Ts...` to implement
-the sorts.
-
-A model `m::Model{Tup}` is marked as implementing a `seg::GATSegment` iff
+Any Julia struct can be a model of a GAT. A model is marked as implementing a 
+`seg::GATSegment` iff
 
 `implements(m, ::Type{Val{gettag(seg)}}) == true`
 
@@ -57,11 +39,26 @@ to get away without providing the context when you are writing code that is not
 across models, and you know that, for instance, composition of FinFunctions does not
 need the domains and codomains of the FinFunctions explicitly supplied.
 
-A model `m::Model{Tup}` implements a theory iff it implements all of the GATSegments
+A model implements a theory iff it implements all of the GATSegments
 in the theory.
-
-Models are defined in TheoryInterface because reasons
 """
+module ModelInterface
+
+export implements, impl_type, TypeCheckFail, SignatureMismatchError, 
+       @model, @instance, @withmodel, @fail, migrate_model, @default_model,
+       Dispatch
+
+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
+
+using MLStyle
+using DataStructures: DefaultDict, OrderedDict
+
 
 """
 `ImplementationNotes`
@@ -75,20 +72,29 @@ struct ImplementationNotes
 end
 
 """
-`implements(m::Model, tag::ScopeTag) -> Union{ImplementationNotes, Nothing}`
+`implements(m::MyModel, tag::ScopeTag) -> Union{ImplementationNotes, Nothing}`
 
 If `m` implements the GATSegment referred to by `tag`, then return the
 corresponding implementation notes.
 """
-implements(m::Module, ::Type{Val{tag}}) where {tag} = nothing
+implements(m, ::Type{Val{tag}}) where {tag} = nothing
 
-implements(m::Model, tag::ScopeTag) = implements(m, Val{tag})
+implements(m, tag::ScopeTag) = implements(m, Val{tag})
 
-implements(m::Model, theory_module::Module) =
+implements(m, theory_module::Module) =
   all(!isnothing(implements(m, gettag(scope))) for scope in theory_module.Meta.theory.segments.scopes)
 
+"""
+If `m` implements a GAT with a type constructor (identified by ident `id`), 
+mapped to a Julia type, this function returns that Julia type.
+"""
+impl_type(m, id::Ident) = impl_type(m, Val{gettag(id)}, Val{getlid(id)})
+
+impl_type(m, mod::Module, name::Symbol) = 
+  impl_type(m, ident(mod.Meta.theory; name))
+
 struct TypeCheckFail <: Exception
-  model::Union{Model, Nothing}
+  model::Any
   theory::GAT
   type::Ident
   val::Any
@@ -108,7 +114,7 @@ end
 Usage:
 
 ```julia
-struct TypedFinSetC <: Model{Tuple{Vector{Int}, Vector{Int}}}
+struct TypedFinSetC
   ntypes::Int
 end
 
@@ -124,11 +130,18 @@ end
   codom(f::Vector{Int}; context) = context.codom
 end
 
-struct SliceCat{Ob, Hom, C <: Model{Tuple{Ob, Hom}}} <: Model{Tuple{Tuple{Ob, Hom}, Hom}}
-  c::C
+struct SliceC{ObT, HomT, C}
+  cat::C
+  over::ObT
+  function SliceC(cat::C, over) where C
+    implements(cat, ThCategory) || error("Bad cat $cat")
+    obtype = impl_type(cat, ThCategory, :Ob)
+    homtype = impl_type(cat, ThCategory, :Hom)
+    new{obtype, homtype, C}(cat, ThCategory.Ob[cat](over))
+  end
 end
 
-@instance ThCategory{Tuple{Ob, Hom}, Hom} [model::SliceCat{Ob, Hom, C}] where {Ob, Hom, C<:Model{Tuple{Ob, Hom}}} begin
+@instance ThCategory{Tuple{Ob, Hom}, Hom} [model::SliceCat{Ob, Hom, C}] where {Ob, Hom, C}}} begin
 end
 ```
 
@@ -210,10 +223,18 @@ function generate_instance(
     []
   end
 
+  impl_type_declarations = if isnothing(model_type) 
+    Expr[]
+  else 
+    map(collect(jltype_by_sort)) do (k, v)
+      impl_type_declaration(model_type, whereparams, k, v)
+    end
+  end
   docsink = gensym(:docsink)
 
   code = Expr(:block,
     [generate_function(f) for f in qualified_functions]...,
+    impl_type_declarations...,
     implements_declarations...,
     :(function $docsink end),
     :(Core.@__doc__ $docsink)
@@ -387,11 +408,7 @@ function typecheck_instance(
 
   overload_errormsg =
    "the types for this model declaration do not permit Julia overloading to distinguish between GAT overloads"
-
   for (decl, resolver) in theory.resolvers
-    if nameof(decl) ∈ ext_functions
-      continue
-    end
     for (_, x) in allmethods(resolver)
       if getvalue(theory[x]) isa AlgStruct 
         continue 
@@ -455,6 +472,7 @@ function typecheck_instance(
   end
 
   for (sig, (decl, method)) in undefined_signatures
+    nameof(decl) ∈ ext_functions && continue # assume it has been impl'd already
     judgment = getvalue(theory[method])
     if judgment isa AlgTermConstructor
       error("Failed to implement $decl: $(toexpr(sig))")
@@ -494,7 +512,9 @@ function mk_fun(f::AlgFunction, theory, mod, jltype_by_sort)
   args = map(zip(f.args, sortsignature(f))) do (i,s)
     Expr(:(::),nameof(f[i]),jltype_by_sort[s])
   end
-  impl = to_call_impl(f.value,theory, mod, false)
+  argnames = Vector{Symbol}(undef, length(getcontext(f)))
+  setindex!.(Ref(argnames), [nameof(f[i]) for i in f.args], getvalue.(f.args))
+  impl = to_call_impl(f.value,theory, mod, argnames, false)
   JuliaFunction(;name=name, args, impl)
 end
 
@@ -517,7 +537,7 @@ function make_alias_definitions(theory, theory_module, jltype_by_sort, model_typ
               args
             end
           else
-            [(gensym(:m), :($(TheoryInterface.WithModel){$model_type})); args]
+            [(gensym(:m), :($(TheoryInterface.WithModel){<:$model_type})); args]
           end
           argexprs = [Expr(:(::), p...) for p in args]
           overload = JuliaFunction(;
@@ -563,7 +583,7 @@ function qualify_function(fun::JuliaFunction, theory_module, model_type::Union{E
 
     m = gensym(:m)
     (
-      [Expr(:(::), m, Expr(:curly, TheoryInterface.WithModel, model_type)), args...],
+      [Expr(:(::), m, Expr(:curly, TheoryInterface.WithModel, Expr(:<:, model_type))), args...],
       Expr(:let, Expr(:(=), :model, :($m.model)), fun.impl)
     )
   else
@@ -581,11 +601,23 @@ function qualify_function(fun::JuliaFunction, theory_module, model_type::Union{E
   )
 end
 
+function impl_type_declaration(model_type, whereparams, sort, jltype)
+  quote 
+    if !hasmethod($(GlobalRef(ModelInterface, :impl_type)), 
+      ($(model_type) where {$(whereparams...)}, Type{Val{$(gettag(getdecl(sort)))}}, Type{Val{$(getlid(getdecl(sort)))}}))
+      $(GlobalRef(ModelInterface, :impl_type))(
+          ::$(model_type), ::Type{Val{$(gettag(getdecl(sort)))}}, ::Type{Val{$(getlid(getdecl(sort)))}}
+        ) where {$(whereparams...)} = $(jltype)
+    end
+  end
+end
+
 function implements_declaration(model_type, scope, whereparams)
   notes = ImplementationNotes(nothing)
+  _, m = methods(implements, (Any, Type{Val{1}})) # first method is for Dispatch
   quote
-    if !hasmethod($(GlobalRef(ModelInterface, :implements)), 
-        ($(model_type) where {$(whereparams...)}, Type{Val{$(gettag(scope))}}))
+    if $m == only(methods($(GlobalRef(ModelInterface, :implements)), 
+        ($(model_type) where {$(whereparams...)}, Type{Val{$(gettag(scope))}})))
       $(GlobalRef(ModelInterface, :implements))(
         ::$(model_type), ::Type{Val{$(gettag(scope))}}
       ) where {$(whereparams...)} = $notes
@@ -630,33 +662,35 @@ macro withmodel(model, subsexpr, body)
 end
 
 
+migrate_model(F::Module, m::Any, new_model_name=nothing) = 
+  migrate_model(F.MAP, m, new_model_name)
+
 """
-Given a Theory Morphism T->U and a model Mᵤ which implements U,
-obtain a model Mₜ which wraps Mᵤ and is a model of T.
+Given a theory map A -> B, construct a new struct type which wraps a model of
+theory B and is itself a model of theory A. The name of the struct can be
+optionally given, otherwise it is gensym'd. The resulting expression is an
+instance of that struct type.
 
 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.
 """
-function migrator(tmap, dom_module, codom_module, dom_theory, codom_theory)
-
-  # Symbols
-  migrator_name = :Migrator # TODO do we need to gensym?
-  _x = gensym("val")
-
-  # Map CODOM sorts to whereparam symbols
-  whereparamdict = OrderedDict(s=>gensym(s.head.name) for s in sorts(codom_theory))
-  # New model is parameterized by these types
-  whereparams = collect(values(whereparamdict))
-  # Julia types of domain sorts determined by theorymap 
+function migrate_model(F::AbsTheoryMap, m::Any, new_model_name::Union{Nothing,Symbol}=nothing)
+  new_model_name = isnothing(new_model_name) ? gensym(:Migrated) : new_model_name
+  dom_theory = dom(F)
+  codom_theory = codom(F)
+  dom_module = GAT_MODULE_LOOKUP[gettag(dom_theory)]
+  codom_module = GAT_MODULE_LOOKUP[gettag(codom_theory)]
+
+  # Expressions which evaluate to the correct Julia type
   jltype_by_sort = Dict(map(sorts(dom_theory)) do v
-    v => whereparamdict[AlgSort(tmap(v.method).val)]
+    v => :(impl_type($m, getdecl(AlgSort($F($v.method).val))))
   end)
 
-  # Create input for instance_code
-  ################################
+  _x = gensym("val")
+
   accessor_funs = JuliaFunction[] # added to during typecon_funs loop
 
-  typecon_funs = map(collect(typemap(tmap))) do (x, fx)
+  typecon_funs = map(collect(typemap(F))) do (x, fx)
     typecon = getvalue(dom_theory[x])
 
     # Accessors
@@ -691,36 +725,37 @@ function migrator(tmap, dom_module, codom_module, dom_theory, codom_theory)
     args = [:($k::$(v)) for (k, v) in zip(argnames, sig.types)]
     
     return_type = first(sig.types)
+    argnames′ = Array{Symbol}(undef, length(getcontext(typecon)))
+    setindex!.(Ref(argnames′), argnames[2:end], getvalue.(typecon.args))
 
-    impls = to_call_impl.(codom_body.args, Ref(codom_theory), Ref(codom_module), true)
+    impls = to_call_impl.(codom_body.args, Ref(codom_theory), Ref(codom_module), 
+                          Ref(argnames′), true)
     impl = Expr(:call, Expr(:ref, :($codom_module.$fxname), 
                             :(model.model)), _x, impls...)
-
     JuliaFunction(;name, args, return_type, impl)
   end
 
-  # Term constructors
-  #------------------
-  termcon_funs = map(collect(termmap(tmap))) do (x, fx)
+
+  termcon_funs = map(collect(termmap(F))) do (x, fx)
     termcon = getvalue(dom_theory[x])
     sig = julia_signature(dom_theory, x, jltype_by_sort)
 
     name = nameof(termcon.declaration)
     return_type = jltype_by_sort[AlgSort(termcon.type)]
-    args = [:($k::$v) for (k, v) in zip(nameof.(argsof(termcon)), sig.types)]
-    impl = to_call_impl(fx.val, codom_theory, codom_module, true)
+    argnames = nameof.(argsof(termcon))
+    argnames′ = Array{Symbol}(undef, length(getcontext(termcon)))
+    setindex!.(Ref(argnames′), argnames, getvalue.(termcon.args))
+    args = [:($k::$v) for (k, v) in zip(argnames, sig.types)]
+    impl = to_call_impl(fx.val, codom_theory, codom_module, argnames′, true)
 
     JuliaFunction(;name, args, return_type, impl)
   end
-
-
-  # Generate instance code 
   instance_code = generate_instance(
     dom_theory,
     dom_module,
     jltype_by_sort,
-    Expr(:curly, migrator_name, whereparams...),
-    whereparams,
+    new_model_name,
+    [],
     Expr(:block, generate_function.([typecon_funs...,
                                      termcon_funs..., 
                                      accessor_funs...
@@ -728,45 +763,32 @@ function migrator(tmap, dom_module, codom_module, dom_theory, codom_theory)
     typecheck=true, escape=false
   )
 
-  tup_params = Expr(:curly, :Tuple, whereparams...)
-
-  model_expr = Expr(
-    :curly,
-    GlobalRef(Syntax.TheoryInterface, :Model),
-    tup_params
-  )
-
-  # The second whereparams needs to be reordered by the sorts of the DOM theory
-  quote
-    struct Migrator{$(whereparams...)} <: $model_expr
-      model ::  $(GlobalRef(ModelInterface, :Model)){$tup_params}
-      function Migrator(model:: $(GlobalRef(ModelInterface, :Model)){$tup_params}) where {$(whereparams...)}
-        $(GlobalRef(ModelInterface, :implements))(model, $codom_module) || error("Cannot migrate model $model")
-        new{$(whereparams...)}(model)
-      end
+  eval(quote 
+    struct $new_model_name 
+      model::Any
     end
-
-    $(instance_code.args...)
-  end
+    $instance_code
+    $new_model_name($m)
+  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, theory::GAT, mod::Union{Symbol,Module}, migrate::Bool)
+function to_call_impl(t::AlgTerm, theory::GAT, mod::Union{Symbol,Module}, argnames::Vector{Symbol}, migrate::Bool)
   b = bodyof(t)
   if GATs.isvariable(t)
-    nameof(b)
+    argnames[getvalue(getlid(b))]
   elseif  GATs.isdot(t)
-    impl = to_call_impl(b.body, theory, mod, migrate)
+    impl = to_call_impl(b.body, theory, mod, argnames, migrate)
     if isnamed(b.head)
       Expr(:., impl, QuoteNode(nameof(b.head)))
     else 
       Expr(:ref, impl, getlid(b.head).val)
     end
   else
-    args = to_call_impl.(argsof(b), Ref(theory), Ref(mod), migrate)
+    args = to_call_impl.(argsof(b), Ref(theory), Ref(mod), Ref(argnames), migrate)
     name = nameof(headof(b))
     newhead = if name ∈ nameof.(structs(theory))
       Expr(:., :($mod), QuoteNode(name))
@@ -784,6 +806,121 @@ function to_call_accessor(t::AlgTerm, x::Symbol, mod::Module)
   Expr(:call, Expr(:ref, :($mod.$(nameof(headof(b)))), :(model.model)), rest)
 end
 
-migrate_model(theorymap::Module, m::Model) = theorymap.Migrator(m)
+
+# Default models
+
+"""
+Create an @instance for a model `M` whose methods are determined by type 
+dispatch, e.g.:
+
+```
+@instance ThCategory{O,H} [model::M] begin
+  id(x::O) = id(x)
+  compose(f::H, g::H)::H = compose(f, g)
+end
+```
+
+Use this with caution! For example, using this with two different models of 
+the same theory with the same types would cause a conflict.
+"""
+function default_instance(theorymodule, theory, jltype_by_sort, model)
+  acc = Iterators.flatten(values.(values(theory.accessors)))
+
+  termcon_funs = map(last.(termcons(theory)) ∪ acc) do x 
+    generate_function(use_dispatch_method_impl(x, theory, jltype_by_sort))
+  end
+  generate_instance(
+    theory, theorymodule, jltype_by_sort, model, [], 
+    Expr(:block, termcon_funs...); typecheck=true, escape=true)
+end
+
+"""
+Create an @instance for a model `M` whose methods are determined by the 
+implementation of another model, `M2`, e.g.:
+
+```
+@instance ThCategory{O,H} [model::M] begin
+  id(x::O) = id[M2](x)
+  compose(f::H, g::H)::H = compose[M2](f, g)
+end
+```
+"""
+function default_model(theorymodule, theory, jltype_by_sort, model)
+  acc = Iterators.flatten(values.(values(theory.accessors)))
+  termcon_funs = map(last.(termcons(theory)) ∪ acc) do x 
+    generate_function(use_model_method_impl(x, theory, jltype_by_sort, model))
+  end
+  generate_instance(
+    theory, theorymodule, jltype_by_sort, nothing, [], 
+    Expr(:block, termcon_funs...); typecheck=true, escape=true)
+end
+
+macro default_model(head, model)
+  # Parse the head of @instance to get theory and instance types
+  (theory_module, instance_types) = @match head begin
+    :($ThX{$(Ts...)}) => (ThX, Ts)
+    _ => error("invalid syntax for head of @instance macro: $head")
+  end
+
+  # Get the underlying theory
+  theory = macroexpand(__module__, :($theory_module.Meta.@theory))
+
+  # A dictionary to look up the Julia type of a type constructor from its name (an ident)
+  jltype_by_sort = Dict{AlgSort,Expr0}([
+    zip(primitive_sorts(theory), instance_types)..., 
+    [s => nameof(headof(s)) for s in struct_sorts(theory)]...
+  ]) 
+
+  # Get the model type that we are overloading for, or nothing if this is the
+  # default instance for `instance_types`
+  m = parse_model_param(model)[1]
+
+  # Create the actual instance
+  default_model(theory_module, theory, jltype_by_sort, m)
+end
+
+"""
+A canonical implementation that just calls the method with the implementation
+of another model, `m`.
+"""
+function use_model_method_impl(x::Ident, theory::GAT, 
+                               jltype_by_sort::Dict{AlgSort}, m::Expr0)
+  op = getvalue(theory[x])
+  name = nameof(getdecl(op))
+  return_type = op isa AlgAccessor ? nothing : jltype_by_sort[AlgSort(op.type)]
+  args = args_from_sorts(sortsignature(op), jltype_by_sort)
+  impl = :(return $(name)[$m()]($(args...)))
+  JuliaFunction(name=name, args=args, return_type=return_type, impl=impl)
+end
+
+"""
+A canonical implementation that just calls the method with type dispatch.
+"""
+function use_dispatch_method_impl(x::Ident, theory::GAT, 
+                                  jltype_by_sort::Dict{AlgSort})
+  op = getvalue(theory[x])
+  name = nameof(getdecl(op))
+  return_type = op isa AlgAccessor ? nothing : jltype_by_sort[AlgSort(op.type)]
+  args = args_from_sorts(sortsignature(op), jltype_by_sort)
+  impl = :(return $(name)($(args...)))
+  JuliaFunction(name=name, args=args, return_type=return_type, impl=impl)
+end
+
+# Special model for any theory which uses dispatch
+##################################################
+
+"""
+Check whether a dispatch model implements a particular scope of a theory.
+This could be more rigorous, like actually checking whether certain methods 
+exist, but for now users will be assuming that the dispatch methods exist when
+using a Dispatch model.
+"""
+function implements(d::Dispatch, ::T) where {X,T <: Type{Val{X}}}
+  hastag(d.t, X) ? true : nothing
+end
+
+function impl_type(d::Dispatch, x::Ident)
+  d.types[AlgSort(x, only(d.t.resolvers[x])[2])]
+end
 
 end # module
diff --git a/src/models/SymbolicModels.jl b/src/models/SymbolicModels.jl
index 26f33c38..d9a180f8 100644
--- a/src/models/SymbolicModels.jl
+++ b/src/models/SymbolicModels.jl
@@ -8,6 +8,7 @@ using ...Util
 using ...Syntax
 import ...Syntax: invoke_term
 using ..ModelInterface
+using ..ModelInterface: args_from_sorts, default_instance
 
 using Base.Meta: ParseError
 using MLStyle
@@ -262,6 +263,10 @@ macro symbolic_model(decl, theoryname, body)
 
   module_structs = symbolic_structs(theory, abstract_types, __module__)
   
+  # Part 1.5: Generate a model  
+  imp = Expr(:import, Expr(:(:), Expr(:., :., :., name), [
+    Expr(:., x) for x in [name, theoryname, name, nameof.(sorts(theory))...]]...))
+
   # Part 2: Generating internal methods
 
   module_methods = [internal_accessors(theory)..., 
@@ -271,15 +276,20 @@ macro symbolic_model(decl, theoryname, body)
     export $(nameof.(sorts(theory))...)
     using ..($(nameof(__module__)))
     import ..($(nameof(__module__))): $theoryname
+
+    $(module_structs...)
+
+    $(generate_function.(module_methods)...)
+
     module $(esc(:Meta))
-      import ..($(name)): $theoryname
+      $imp
       const $(esc(:theory_module)) = $(esc(theoryname))
       const $(esc(:theory)) = $(theory)
       const $(esc(:theory_type)) = $(esc(theoryname)).Meta.T
+      # Canonical symbolic model
+      $(esc(:M)) = Dispatch($(esc(:theory)), [$(esc.(nameof.(theory.sorts))...)])
     end
 
-    $(module_structs...)
-    $(generate_function.(module_methods)...)
   end)
 
   # Part 3: Generating instance of theory
@@ -731,4 +741,4 @@ function show_latex_script(io::IO, expr::GATExpr, head::String;
   print(io, "}")
 end
 
-end
+end # module
diff --git a/src/nonstdlib/models/Pushouts.jl b/src/nonstdlib/models/Pushouts.jl
index 5c9def88..33fb6376 100644
--- a/src/nonstdlib/models/Pushouts.jl
+++ b/src/nonstdlib/models/Pushouts.jl
@@ -2,8 +2,6 @@ using DataStructures, StructEquality
 
 export PushoutInt
 
-using GATlab
-
 """Data required to specify a pushout. No fancy caching."""
 @struct_hash_equal struct PushoutInt
   ob::Int
diff --git a/src/stdlib/derivedmodels/DerivedModels.jl b/src/stdlib/derivedmodels/DerivedModels.jl
index a75674ba..5287ebc2 100644
--- a/src/stdlib/derivedmodels/DerivedModels.jl
+++ b/src/stdlib/derivedmodels/DerivedModels.jl
@@ -6,7 +6,7 @@ using ...StdTheoryMaps
 using ...StdModels
 
 # Given a model of a category C, we can derive a model of Cᵒᵖ.
-OpFinSetC = migrate_model(OpCat, FinSetC())
+OpFinSetC = migrate_model(OpCat, FinSetC(), :OpFinSetCat)
 
 # Interpret `e` as `0` and `⋅` as `+`.
 IntMonoid = migrate_model(NatPlusMonoid, IntNatPlus())
diff --git a/src/stdlib/models/arithmetic.jl b/src/stdlib/models/arithmetic.jl
index 76c53a17..9e5c0e04 100644
--- a/src/stdlib/models/arithmetic.jl
+++ b/src/stdlib/models/arithmetic.jl
@@ -3,14 +3,14 @@ export IntNat, IntNatPlus, IntPreorder, ZRing, BoolRing
 using ...Models
 using ..StdTheories
 
-struct IntNat <: Model{Tuple{Int}} end
+struct IntNat end
 
 @instance ThNat{Int} [model::IntNat] begin
   Z() = 0
   S(n::Int) = n + 1
 end
 
-struct IntNatPlus <: Model{Tuple{Int}} end
+struct IntNatPlus end
 
 @instance ThNatPlus{Int} [model::IntNatPlus] begin
   Z() = 0
@@ -18,7 +18,7 @@ struct IntNatPlus <: Model{Tuple{Int}} end
   +(x::Int, y::Int) = x + y
 end
 
-struct IntPreorder <: Model{Tuple{Int, Tuple{Int,Int}}} end
+struct IntPreorder 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])"
@@ -30,7 +30,7 @@ struct IntPreorder <: Model{Tuple{Int, Tuple{Int,Int}}} end
   end
 end
 
-struct ZRing <: Model{Tuple{Int}} end
+struct ZRing end
 
 @instance ThRing{Int} [model::ZRing] begin
   zero() = 0
diff --git a/src/stdlib/models/finmatrices.jl b/src/stdlib/models/finmatrices.jl
index 35051d07..1d8d380a 100644
--- a/src/stdlib/models/finmatrices.jl
+++ b/src/stdlib/models/finmatrices.jl
@@ -3,8 +3,7 @@ export FinMatC
 using ...Models
 using ..StdTheories
 
-struct FinMatC{T<:Number} <: Model{Tuple{T}}
-end
+struct FinMatC{T <: Number} end
 
 @instance ThCategory{Int, Matrix{T}} [model::FinMatC{T}] where {T} begin
   Ob(n::Int) = n >= 0 ? n : @fail "expected nonnegative integer"
diff --git a/src/stdlib/models/finsets.jl b/src/stdlib/models/finsets.jl
index 2820eb92..eb2f1905 100644
--- a/src/stdlib/models/finsets.jl
+++ b/src/stdlib/models/finsets.jl
@@ -3,8 +3,7 @@ export FinSetC
 using ...Models
 using ..StdTheories
 
-struct FinSetC <: Model{Tuple{Int, Vector{Int}}}
-end
+struct FinSetC end
 
 @instance ThCategory{Int, Vector{Int}} [model::FinSetC] begin
   Ob(x::Int) = x >= 0 ? x : @fail "expected nonnegative integer"
diff --git a/src/stdlib/models/gats.jl b/src/stdlib/models/gats.jl
index 8d6cc87e..db2ed9a0 100644
--- a/src/stdlib/models/gats.jl
+++ b/src/stdlib/models/gats.jl
@@ -4,10 +4,7 @@ using ...Models
 using ...Syntax
 using ..StdTheories
 
-using GATlab, GATlab.Models
-
-struct GATC <: Model{Tuple{GAT, AbsTheoryMap}}
-end
+struct GATC end
 
 @instance ThCategory{GAT, AbsTheoryMap} [model::GATC] begin
   id(x::GAT) = IdTheoryMap(x)
diff --git a/src/stdlib/models/nothings.jl b/src/stdlib/models/nothings.jl
index 3a7fac67..90d851af 100644
--- a/src/stdlib/models/nothings.jl
+++ b/src/stdlib/models/nothings.jl
@@ -2,8 +2,7 @@ export NothingC
 
 using ...Models, ..StdTheories
 
-struct NothingC <: Model{Tuple{Nothing, Nothing}}
-end
+struct NothingC end
 
 @instance ThCategory{Nothing, Nothing} [model::NothingC] begin
   Ob(::Nothing) = nothing
diff --git a/src/stdlib/models/op.jl b/src/stdlib/models/op.jl
index e0e346f9..2d973a34 100644
--- a/src/stdlib/models/op.jl
+++ b/src/stdlib/models/op.jl
@@ -10,8 +10,17 @@ using ...Models
 using ..StdTheories
 using StructEquality
 
-@struct_hash_equal struct OpC{ObT, HomT, C<:Model{Tuple{ObT, HomT}}} <: Model{Tuple{ObT, HomT}}
-  cat::C
+# TODO when we implement custom structs for models of a particular theory, we 
+# can use that rather than a generic "C" for which we then have to check 
+# whether it implements the theory.
+
+@struct_hash_equal struct OpC{ObT, HomT, C}
+  cat::C 
+  function OpC(c::C) where C 
+    obtype = impl_type(c, ThCategory, :Ob)
+    homtype = impl_type(c, ThCategory, :Hom)
+    implements(c, ThCategory) ? new{obtype, homtype, C}(c) : error("bad")
+  end
 end
 
 op(c) = OpC(c)
diff --git a/src/stdlib/models/slicecategories.jl b/src/stdlib/models/slicecategories.jl
index 923ab998..701d172e 100644
--- a/src/stdlib/models/slicecategories.jl
+++ b/src/stdlib/models/slicecategories.jl
@@ -9,13 +9,15 @@ using StructEquality
   hom::HomT
 end
 
-@struct_hash_equal struct SliceC{ObT, HomT, C<:Model{Tuple{ObT, HomT}}} <: Model{Tuple{SliceOb{ObT, HomT}, HomT}}
+@struct_hash_equal struct SliceC{ObT, HomT, C}
   cat::C
   over::ObT
-  # function SliceC(cat, over)
-  #   implements(cat, ThCategory)
-  #   new(cat, Ob[cat](over))
-  # end
+  function SliceC(cat::C, over) where C
+    implements(cat, ThCategory) || error("Bad cat $cat")
+    obtype = impl_type(cat, ThCategory, :Ob)
+    homtype = impl_type(cat, ThCategory, :Hom)
+    new{obtype, homtype, C}(cat, ThCategory.Ob[cat](over))
+  end
 end
 
 using .ThCategory
diff --git a/src/syntax/GATs.jl b/src/syntax/GATs.jl
index 19326a16..e2c54d3c 100644
--- a/src/syntax/GATs.jl
+++ b/src/syntax/GATs.jl
@@ -14,7 +14,7 @@ export Constant, AlgTerm, AlgType, AlgAST,
 using ..Scopes
 import ..ExprInterop: fromexpr, toexpr
 
-import ..Scopes: retag, rename, reident
+import ..Scopes: retag, rename, reident, gettag
 
 import AlgebraicInterfaces: equations
 
diff --git a/src/syntax/TheoryInterface.jl b/src/syntax/TheoryInterface.jl
index 8eb50f97..8fc1d7de 100644
--- a/src/syntax/TheoryInterface.jl
+++ b/src/syntax/TheoryInterface.jl
@@ -1,14 +1,11 @@
 module TheoryInterface
-export @theory, @signature, Model, invoke_term
+export @theory, @signature, invoke_term
 
 using ..Scopes, ..GATs, ..ExprInterop, GATlab.Util
-# using GATlab.Util
 
 using MLStyle, StructEquality, Markdown
 
-abstract type Model{Tup <: Tuple} end
-
-@struct_hash_equal struct WithModel{M <: Model}
+@struct_hash_equal struct WithModel{M}
   model::M
 end
 
@@ -153,11 +150,13 @@ 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...)
 
   push!(modulelines, Expr(:toplevel, :(module Meta
     struct T end
    
-    @doc ($(Markdown.MD)((@doc $(__module__).$doctarget), $docstr))
     const theory = $theory
 
     macro theory() $theory end
@@ -180,17 +179,33 @@ function theory_impl(head, body, __module__)
         $(structlines...)
         end
       ),
-      :(@doc ($(Markdown.MD)((@doc $doctarget), $docstr)) $name)
+      :(@doc ($(Markdown.MD)($mdp(@doc $doctarget), $docstr)) $name)
     )
   )
 end
 
+"""
+The Dispatch type is a model of every theory.
+"""
+@struct_hash_equal struct Dispatch 
+  t::GAT
+  types::Dict{AlgSort,Type}
+end
+
+Dispatch(t::GAT, v::AbstractVector{<:Type}) = 
+  Dispatch(t, Dict(zip(sorts(t), v)))
+
+# WARNING: if any other package play with indexing methodnames with their own 
+# structs, then this code could be broken because it assumes we are the only  
+# ones to use this trick.
 function juliadeclaration(name::Symbol)
   quote
     function $name end
+    # we expect just one method because of Dispatch type
+    if isempty(Base.methods(Base.getindex, [typeof($name), Any]))
+      Base.getindex(f::typeof($name), ::$(GlobalRef(TheoryInterface, :Dispatch))) = f
 
-    if Base.isempty(Base.methods(Base.getindex, [typeof($name), $(GlobalRef(TheoryInterface, :Model))]))
-      function Base.getindex(::typeof($name), m::$(GlobalRef(TheoryInterface, :Model)))
+      function Base.getindex(::typeof($name), m::Any) 
         (args...; context=nothing) -> $name($(GlobalRef(TheoryInterface, :WithModel))(m), args...; context)
       end
     end
diff --git a/src/syntax/TheoryMaps.jl b/src/syntax/TheoryMaps.jl
index fae0f915..4364dfef 100644
--- a/src/syntax/TheoryMaps.jl
+++ b/src/syntax/TheoryMaps.jl
@@ -402,8 +402,6 @@ macro theorymap(head, body)
   codom = macroexpand(__module__, :($codomname.Meta.@theory))
   tmap = fromexpr(dom, codom, body, TheoryMap)
 
-  mig = migrator(tmap, dommod, codommod, dom, codom)
-
   esc(
     Expr(
       :toplevel,
@@ -413,8 +411,6 @@ macro theorymap(head, body)
           macro map() $tmap end
           macro dom() $dommod end
           macro codom() $codommod end
-
-          $mig
         end
       ),
       :(Core.@__doc__ $(name)),
diff --git a/src/syntax/gats/gat.jl b/src/syntax/gats/gat.jl
index eb6841a6..4dc8ed92 100644
--- a/src/syntax/gats/gat.jl
+++ b/src/syntax/gats/gat.jl
@@ -36,6 +36,8 @@ fancier.
   bysignature::Dict{AlgSorts, Ident}
 end
 
+Base.iterate(m::MethodResolver, i...) = iterate(m.bysignature, i...)
+
 function MethodResolver()
   MethodResolver(Dict{AlgSorts, Ident}())
 end
@@ -379,3 +381,5 @@ end
 
 """Get all structs in a theory"""
 structs(t::GAT) = AlgStruct[getvalue(t[methodof(s)]) for s in struct_sorts(t)]
+
+gettag(T::GAT) = gettag(T.segments.scopes[end])
diff --git a/test/models/ModelInterface.jl b/test/models/ModelInterface.jl
index 55181643..185575eb 100644
--- a/test/models/ModelInterface.jl
+++ b/test/models/ModelInterface.jl
@@ -1,11 +1,8 @@
 module TestModelInterface 
 
-using GATlab
-using Test
-using StructEquality
+using GATlab, Test, StructEquality
 
-@struct_hash_equal struct FinSetC <: Model{Tuple{Int, Vector{Int}}}
-end
+@struct_hash_equal struct FinSetC end
 
 @instance ThCategory{Int, Vector{Int}} [model::FinSetC] begin
   # check f is Hom: n -> m
@@ -56,9 +53,10 @@ end
 @test_throws ErrorException codom[FinSetC()]([1,2,3])
 
 @test implements(FinSetC(), ThCategory)
+@test !implements(FinSetC(), ThNatPlus)
 
 # Todo: get things working where Ob and Hom are the same type (i.e. binding dict not monic)
-struct TypedFinSetC <: Model{Tuple{Vector{Int}, Vector{Int}}}
+@struct_hash_equal struct TypedFinSetC
   ntypes::Int
 end
 
@@ -170,4 +168,65 @@ end
   munit() = 0
 end
 
+# Test scenario where we @import a method but then extend it
+############################################################
+@theory T1 begin 
+  X::TYPE; 
+  h(a::X)::X 
+end
+
+@theory T2<:T1 begin 
+  Y::TYPE; 
+  h(b::Y)::Y 
+end
+
+@instance T1{Int} begin 
+  h(a::Int) = 1 
+end
+
+@instance T2{Int,Bool} begin 
+  @import X, h
+  h(b::Bool) = false 
+end
+
+@test h(2) == 1
+
+@test h(false) == false
+
+# Test models with abstract types 
+#################################
+ 
+""" Assume this implements Base.iterate """
+abstract type MyAbsIter{V} end
+
+struct MyVect{V} <: MyAbsIter{V}
+  v::Vector{V}
+end
+
+Base.iterate(m::MyVect, i...) = iterate(m.v, i...)
+
+@instance ThSet{V} [model::MyAbsIter{V}] where V begin 
+  default(v::V) = v ∈ model ? v : @fail "Bad $v not in $model"
+end
+
+@test implements(MyVect([1,2,3]), ThSet)
+
+# this will fail unless WithModel accepts subtypes
+@test ThSet.default[MyVect([1,2,3])](1) == 1
+
+# Test default model + dispatch model
+#####################################
+@test_throws MethodError id(2)
+
+@default_model ThCategory{Int, Vector{Int}} [model::FinSetC]
+
+d = Dispatch(ThCategory.Meta.theory, [Int, Vector{Int}])
+@test implements(d, ThCategory)
+@test !implements(d, ThNatPlus)
+@test impl_type(d, ThCategory, :Ob) == Int 
+@test impl_type(d, ThCategory, :Hom) == Vector{Int} 
+
+@test id(2) == [1,2] == ThCategory.id[d](2)
+@test compose([1,2,3], [2,1,3]) == [2,1,3]
+ 
 end # module
diff --git a/test/models/SymbolicModels.jl b/test/models/SymbolicModels.jl
index 61271e32..b37684cf 100644
--- a/test/models/SymbolicModels.jl
+++ b/test/models/SymbolicModels.jl
@@ -19,6 +19,15 @@ f = FreeCategory.Hom{:generator}([:f], [x, y])
 @test ThCategory.id(x) isa HomExpr{:id}
 @test ThCategory.compose(ThCategory.id(x), f) == f
 
+M = FreeCategory.Meta.M
+@test M isa Dispatch
+@test implements(M, ThCategory)
+@test !implements(M, ThNatPlus)
+@test impl_type(M, ThCategory, :Ob) == FreeCategory.Ob
+@test impl_type(M, ThCategory, :Hom) == FreeCategory.Hom
+@test ThCategory.id[M](x) isa HomExpr{:id}
+@test ThCategory.compose[M](ThCategory.id(x), f) == f
+
 # Monoid
 ########
 
diff --git a/test/stdlib/FinMatrices.jl b/test/stdlib/FinMatrices.jl
index 4bce8cce..c1376bd1 100644
--- a/test/stdlib/FinMatrices.jl
+++ b/test/stdlib/FinMatrices.jl
@@ -20,4 +20,7 @@ using .ThCategory
 
 end
 
-end
+# Test that `impl_type` is sensitive to the `where` parameters
+@test impl_type(FinMatC{Float64}(), ThCategory, :Hom) == Matrix{Float64}
+
+end # module
diff --git a/test/stdlib/FinSets.jl b/test/stdlib/FinSets.jl
index 7887388e..fd81b07b 100644
--- a/test/stdlib/FinSets.jl
+++ b/test/stdlib/FinSets.jl
@@ -16,4 +16,4 @@ using .ThCategory
   @test codom([5]; context=(codom=10,)) == 10
 end
 
-end
+end # module
diff --git a/test/stdlib/Nothings.jl b/test/stdlib/Nothings.jl
index 2cae9977..a199bc00 100644
--- a/test/stdlib/Nothings.jl
+++ b/test/stdlib/Nothings.jl
@@ -13,4 +13,4 @@ using .ThCategory
   @test isnothing(compose(nothing, nothing))
 end
 
-end
+end # module
diff --git a/test/stdlib/Op.jl b/test/stdlib/Op.jl
index b0e698f2..905dab0b 100644
--- a/test/stdlib/Op.jl
+++ b/test/stdlib/Op.jl
@@ -35,5 +35,4 @@ end
   @test codom([5]) == 1
 end
 
-
 end # module
diff --git a/test/stdlib/SliceCategories.jl b/test/stdlib/SliceCategories.jl
index 046b706d..f428f836 100644
--- a/test/stdlib/SliceCategories.jl
+++ b/test/stdlib/SliceCategories.jl
@@ -2,7 +2,7 @@ module TestSliceCategories
 
 using GATlab, Test
 
-const C = SliceC{Int, Vector{Int}, FinSetC}(FinSetC(), 4)
+const C = SliceC(FinSetC(), 4)
 const MkOb = SliceOb{Int, Vector{Int}}
 
 using .ThCategory
diff --git a/test/syntax/TheoryInterface.jl b/test/syntax/TheoryInterface.jl
index 652719b9..da5ec349 100644
--- a/test/syntax/TheoryInterface.jl
+++ b/test/syntax/TheoryInterface.jl
@@ -46,7 +46,8 @@ end
   @op 1 + 1
 end
 
-@test (@doc ThCMonoid.Meta.theory) isa Markdown.MD
-@test (@doc ThSet) == (@doc ThSet.Meta.theory)
+# DEPRECATED
+# @test (@doc ThCMonoid.Meta.theory) isa Markdown.MD
+# @test (@doc ThSet) == (@doc ThSet.Meta.theory)
 
 end