Declaring models

[olynch]

This is my proposed syntax for declaring singleton models families (i.e., models which are indexed by zero-field structs)

@model_single Category FinSetC{Int, Vector{Int}} begin
  Ob(x::Int) = true
  Hom(x::Int, y::Int, f::Vector{Int}) = length(f) == x && all(1 <= j <= y for j in f)

  compose(f::Vector{Int}, g::Vector{Int}; context...) = Int[g[j] for j in f]
  id(x::Int) = collect(1:x)
end

For a model family, I'm imagining that you declare the struct manually, and then call a macro to declare the relevant methods.

struct TypedFinSetC <: Model{Category.Th, Tuple{Vector{Int}, Vector{Int}}}
  ntypes::Int
end

@model_family Category TypedFinSetC begin
  Ob(m::TypedFinSetC, v::Vector{Int}) = all(1 <= j <= m.types for j in v)
  Hom(::TypedFinSetC, x::Vector{Int}, y::Vector{Int}, f::Vector{Int}) = length(f) == length(x) &&
    all(1 <= j <= length(y) for j in f) &&
    all(x[i] == y[f[i]] for i in 1:length(x))

  compose(::TypedFinSetC, f::Vector{Int}, g::Vector{Int}; context...) = Int[g[j] for j in f]
  id(::TypedFinSetC, v::Vector{Int}) = collect(1:length(v))
end

[olynch]

Closing this as this syntax evolves to make it clear this is out of date.