Although we cannot statically check whether a given type is a model of a theory (as this depends on which methods are defined), we can check this at runtime. Nevertheless, it is helpful when writing code that works with models of GATs to make explicit at the type level "I am expecting something that can implement the ThCategory interface".

In practice I've found one nice solution to this is the idea of a smart constructor. For example:

struct Category
  val::Any 
  Category(x::Any) = implements(x, ThCategory) ? new(x) : error("Bad $x")
end

getvalue(c::Category) = c.val

The @theory macro could programmatically generate and bind a structure to ThWhatever.Meta.Wrapper for any theory. We would want some other methods defined for it too in order to be ergonomic:

id(c::Category, x) = id[getvalue(c)](x)
compose(c::Category, f, g) = compose[getvalue(c)](f, g)
# and so on for the type constructors and accessors
impl_type(c::Category, x...) = impl_type(getvalue(c), x...)

Although this isn't the direction Catlab is moving in, at times it might be nice to not have to get the impl_type at runtime: there's also the possibility of generating another wrapper struct:

struct Category′{Ob,Hom}
  val::Any 
  function Category′(x::Any) 
    implements(x, ThCategory) || error("Bad $x")
   new{impl_type(x, ThCategory, :Ob), impl_type(x, ThCategory, :Hom)}(x)
  end
end

Such that we could wrap SkelFinSetC() and get a Category′{Int,Vector{Int}}.