diff --git a/src/models/ModelInterface.jl b/src/models/ModelInterface.jl
index 7e0e957c..f3388ba9 100644
--- a/src/models/ModelInterface.jl
+++ b/src/models/ModelInterface.jl
@@ -109,7 +109,7 @@ struct TypedFinSetC <: Model{Tuple{Vector{Int}, Vector{Int}}}
   ntypes::Int
 end
 
-@instance ThCategory{Vector{Int}, Vector{Int}} (;model::TypedFinSetC) begin
+@instance ThCategory{Vector{Int}, Vector{Int}} [model::TypedFinSetC] begin
   Ob(v::Vector{Int}) = all(1 <= j <= model.ntypes for j in v)
   Hom(f::Vector{Int}, v::Vector{Int}, w::Vector{Int}) =
      length(f) == length(v) && all(1 <= y <= length(w) for y in f)
@@ -125,7 +125,7 @@ struct SliceCat{Ob, Hom, C <: Model{Tuple{Ob, Hom}}} <: Model{Tuple{Tuple{Ob, Ho
   c::C
 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<:Model{Tuple{Ob, Hom}}} begin
 end
 ```
 
@@ -191,7 +191,7 @@ function parse_model_param(e)
   end
 
   model_type = @match paramdecl begin
-    Expr(:tuple, Expr(:parameters, Expr(:(::), :model, model_type))) => model_type
+    Expr(:vect, Expr(:(::), :model, model_type)) => model_type
     nothing => nothing
     _ => error("invalid syntax for declaring model type: $model")
   end
diff --git a/src/stdlib/models/FinMatrices.jl b/src/stdlib/models/FinMatrices.jl
index d6afe220..5d6a6b48 100644
--- a/src/stdlib/models/FinMatrices.jl
+++ b/src/stdlib/models/FinMatrices.jl
@@ -7,7 +7,7 @@ using ...StdTheories
 struct FinMatC{T<:Number} <: Model{Tuple{T}}
 end
 
-@instance ThCategory{Int, Matrix{T}} (;model::FinMatC{T}) where {T} begin
+@instance ThCategory{Int, Matrix{T}} [model::FinMatC{T}] where {T} begin
   Ob(n::Int) = n >= 0 ? n : @fail "expected nonnegative integer"
   Hom(A::Matrix{T}, n::Int, m::Int) =
     size(A) == (n,m) ? A : @fail "expected dimensions to be $((n,m))"
diff --git a/src/stdlib/models/FinSets.jl b/src/stdlib/models/FinSets.jl
index 880dcce1..8d9aa3ea 100644
--- a/src/stdlib/models/FinSets.jl
+++ b/src/stdlib/models/FinSets.jl
@@ -7,7 +7,7 @@ using ...StdTheories
 struct FinSetC <: Model{Tuple{Int, Vector{Int}}}
 end
 
-@instance ThCategory{Int, Vector{Int}} (;model::FinSetC) begin
+@instance ThCategory{Int, Vector{Int}} [model::FinSetC] begin
   Ob(x::Int) = x >= 0 ? x : @fail "expected nonnegative integer"
 
   function Hom(f::Vector{Int}, n::Int, m::Int)
diff --git a/src/stdlib/models/GATs.jl b/src/stdlib/models/GATs.jl
index 7fa6e8d0..2d082f8e 100644
--- a/src/stdlib/models/GATs.jl
+++ b/src/stdlib/models/GATs.jl
@@ -10,7 +10,7 @@ using GATlab, GATlab.Models
 struct GATC <: Model{Tuple{GAT, AbsTheoryMap}}
 end
 
-@instance ThCategory{GAT, AbsTheoryMap} (;model::GATC) begin
+@instance ThCategory{GAT, AbsTheoryMap} [model::GATC] begin
   id(x::GAT) = IdTheoryMap(x)
   compose(f::AbsTheoryMap, g::AbsTheoryMap) = TheoryMaps.compose(f,g)
   dom(f::AbsTheoryMap) = TheoryMaps.dom(f)
diff --git a/src/stdlib/models/Nothings.jl b/src/stdlib/models/Nothings.jl
index d5b381ab..a2150225 100644
--- a/src/stdlib/models/Nothings.jl
+++ b/src/stdlib/models/Nothings.jl
@@ -6,7 +6,7 @@ using ....Models, ...StdTheories
 struct NothingC <: Model{Tuple{Nothing, Nothing}}
 end
 
-@instance ThCategory{Nothing, Nothing} (;model::NothingC) begin
+@instance ThCategory{Nothing, Nothing} [model::NothingC] begin
   Ob(::Nothing) = nothing
   Hom(::Nothing, ::Nothing, ::Nothing) = nothing
 
diff --git a/src/stdlib/models/SliceCategories.jl b/src/stdlib/models/SliceCategories.jl
index a133aa53..f2ea45dc 100644
--- a/src/stdlib/models/SliceCategories.jl
+++ b/src/stdlib/models/SliceCategories.jl
@@ -17,15 +17,15 @@ end
 
 using .ThCategory
 
-@instance ThCategory{SliceOb{ObT, HomT}, HomT} (;model::SliceC{ObT, HomT, C}) where {ObT, HomT, C} begin
+@instance ThCategory{SliceOb{ObT, HomT}, HomT} [model::SliceC{ObT, HomT, C}] where {ObT, HomT, C} begin
   function Ob(x::SliceOb{ObT, HomT})
     try
-      Ob(x.ob; model=model.cat)
+      Ob[model.cat](x.ob)
     catch e
       @fail ("ob is not valid", e)
     end
     try
-      Hom(x.hom, x.ob, model.over; model=model.cat)
+      Hom[model.cat](x.hom, x.ob, model.over)
     catch e
       @fail ("hom is not valid", e)
     end
@@ -36,19 +36,19 @@ using .ThCategory
 
   function Hom(f::HomT, x::SliceOb{ObT, HomT}, y::SliceOb{ObT, HomT})
     try
-      Hom(f, x.ob, y.ob; model=model.cat)
+      Hom[model.cat](f, x.ob, y.ob)
     catch e
       @fail ("morphism is not valid in base category", e)
     end
-    compose(f, y.hom; model=model.cat, context=(a=x.ob, b=y.ob, c=model.over)) == x.hom ||
+    compose[model.cat](f, y.hom; context=(a=x.ob, b=y.ob, c=model.over)) == x.hom ||
       @fail "commutativity of triangle does not hold"
     f
   end
 
-  id(x::SliceOb{ObT, HomT}) = id(x.ob; model=model.cat)
+  id(x::SliceOb{ObT, HomT}) = id[model.cat](x.ob)
 
   compose(f::HomT, g::HomT; context=nothing) =
-    compose(f, g; model=model.cat, context=isnothing(context) ? nothing : map(x -> x.ob, context))
+    compose[model.cat](f, g; context=isnothing(context) ? nothing : map(x -> x.ob, context))
 end
 
 end
diff --git a/src/syntax/TheoryInterface.jl b/src/syntax/TheoryInterface.jl
index 6522864c..22125d65 100644
--- a/src/syntax/TheoryInterface.jl
+++ b/src/syntax/TheoryInterface.jl
@@ -72,13 +72,13 @@ macro theory(head, body)
     # TODO: also push an automatically generated docstring
     push!(
       modulelines,
-      :(function $name(args...; model=nothing, context=nothing)
-          if !isnothing(model)
-            $name($(WithModel)(model), args...; context)
-          else
-            throw(MethodError($name, args))
-          end
-        end)
+      quote
+        function $name end
+
+        function Base.getindex(::typeof($name), m::$(GlobalRef(TheoryInterface, :Model)))
+          (args...; context=nothing) -> $name($(GlobalRef(TheoryInterface, :WithModel))(m), args...; context)
+        end
+      end
     )
   end
 
diff --git a/test/models/ModelInterface.jl b/test/models/ModelInterface.jl
index 76fcc476..a4e4f16c 100644
--- a/test/models/ModelInterface.jl
+++ b/test/models/ModelInterface.jl
@@ -7,7 +7,7 @@ using StructEquality
 @struct_hash_equal struct FinSetC <: Model{Tuple{Int, Vector{Int}}}
 end
 
-@instance ThCategory{Int, Vector{Int}} (;model::FinSetC) begin
+@instance ThCategory{Int, Vector{Int}} [model::FinSetC] begin
   # check f is Hom: n -> m
   function Hom(f::Vector{Int}, n::Int, m::Int)
     if length(f) == n
@@ -30,12 +30,12 @@ end
 
 using .ThCategory
 
-@test Ob(-1; model=FinSetC()) == -1
-@test Hom([1,2,3], 3, 3; model=FinSetC()) == [1,2,3]
-@test_throws TypeCheckFail Hom([1,2,3], 3, 2; model=FinSetC())
+@test Ob[FinSetC()](-1) == -1
+@test Hom[FinSetC()]([1,2,3], 3, 3) == [1,2,3]
+@test_throws TypeCheckFail Hom[FinSetC()]([1,2,3], 3, 2)
 
 try
-  ThCategory.Hom([1,2,3], 3, 2; model=FinSetC())
+  ThCategory.Hom[FinSetC()]([1,2,3], 3, 2)
 catch e
   @test e.model == FinSetC()
   @test e.theory == ThCategory.THEORY
@@ -46,14 +46,14 @@ catch e
   @test sprint(showerror, e) isa String
 end
 
-@test_throws TypeCheckFail Hom([1,2,3], 3, 2; model=FinSetC())
-@test_throws TypeCheckFail Hom([1,2,3], 2, 3; model=FinSetC())
-@test compose([1,3,2], [1,3,2]; model=FinSetC()) == [1,2,3]
+@test_throws TypeCheckFail Hom[FinSetC()]([1,2,3], 3, 2)
+@test_throws TypeCheckFail Hom[FinSetC()]([1,2,3], 2, 3)
+@test compose[FinSetC()]([1,3,2], [1,3,2]) == [1,2,3]
 
-@test id(2; model=FinSetC()) == [1,2]
+@test id[FinSetC()](2) == [1,2]
 
-@test dom([1,2,3]; model=FinSetC()) == 3
-@test_throws ErrorException codom([1,2,3]; model=FinSetC())
+@test dom[FinSetC()]([1,2,3]) == 3
+@test_throws ErrorException codom[FinSetC()]([1,2,3])
 
 @test implements(FinSetC(), ThCategory)
 
@@ -62,7 +62,7 @@ struct TypedFinSetC <: Model{Tuple{Vector{Int}, Vector{Int}}}
   ntypes::Int
 end
 
-@instance ThStrictMonCat{Int, Vector{Int}} (;model::FinSetC) begin
+@instance ThStrictMonCat{Int, Vector{Int}} [model::FinSetC] begin
   @import Ob, Hom, id, compose, dom, codom
 
   mcompose(a::Int, b::Int) = a + b
@@ -75,8 +75,8 @@ end
 
 using .ThStrictMonCat
 
-@test mcompose(id(2; model=FinSetC()), id(2; model=FinSetC()); context=(;B₁=2), model=FinSetC()) ==
-  id(4; model=FinSetC())
+@test mcompose[FinSetC()](id[FinSetC()](2), id[FinSetC()](2); context=(;B₁=2)) ==
+  id[FinSetC()](4)
 
 @struct_hash_equal struct FinSet 
   n::Int 
@@ -87,7 +87,7 @@ end
   dom::FinSet 
   codom::FinSet
   function FinFunction(values::AbstractVector, dom::FinSet, codom::FinSet)
-    new(ThCategory.Hom(Vector{Int}(values), dom.n, codom.n; model=FinSetC()), dom, codom)
+    new(ThCategory.Hom[FinSetC()](Vector{Int}(values), dom.n, codom.n), dom, codom)
   end
 end 
 
@@ -127,22 +127,22 @@ end
 
 @test_throws MethodError id(2)
 
-@test_throws LoadError @eval @instance ThCategory{Int, Vector{Int}} (;model::FinSetC) begin
+@test_throws LoadError @eval @instance ThCategory{Int, Vector{Int}} [model::FinSetC] begin
 end
 
-@test_throws LoadError @eval @instance ThCategory{Int, Vector{Int}} (;model::FinSetC) begin
+@test_throws LoadError @eval @instance ThCategory{Int, Vector{Int}} [model::FinSetC] begin
   compose(f::Vector{Int}, g::Vector{Int}) = g[f]
   dom(f::Vector{Int}) = length(f)
 end
 
-@test_throws LoadError @eval @instance ThCategory{Int, Vector{Int}} (;model::FinSetC) begin
+@test_throws LoadError @eval @instance ThCategory{Int, Vector{Int}} [model::FinSetC] begin
   id(f::Vector{Int}) = f
   compose(f::Vector{Int}, g::Vector{Int}) = g[f]
   dom(f::Vector{Int}) = length(f)
 end
 
 try
-  @eval @instance ThCategory{Int, Vector{Int}} (;model::FinSetC) begin
+  @eval @instance ThCategory{Int, Vector{Int}} [model::FinSetC] begin
     id(f::Vector{Int}) = f
     compose(f::Vector{Int}, g::Vector{Int}) = g[f]
     dom(f::Vector{Int}) = length(f)
@@ -152,7 +152,7 @@ catch e
   @test sprint(showerror, e.error) isa String
 end
 
-@test_throws LoadError @eval @instance ThStrictMonCat{Int, Vector{Int}} (;model::FinSetC) begin
+@test_throws LoadError @eval @instance ThStrictMonCat{Int, Vector{Int}} [model::FinSetC] begin
   @import Ob, Hom, id, compose, dom, codom
 
   mcompose(f::Vector{Int}, g::Vector{Int}; context) = [f; g .+ context.B₁]
@@ -160,7 +160,7 @@ end
   munit() = 0
 end
 
-@test_throws LoadError @eval @instance ThStrictMonCat{Int, Int} (;model::FinSetC) begin
+@test_throws LoadError @eval @instance ThStrictMonCat{Int, Int} [model::FinSetC] begin
   @import Ob, Hom, id, compose, dom, codom
 
   mcompose(a::Int, b::Int) = a + b