Morphisms in data category of ACSet schemas

[epatters]

The data category in the schema is assumed to be discrete, but it would helpful to allow the specification of morphisms.

For example, the schema for a free diagram is currently as defined:

@present TheoryFreeDiagram <: TheoryGraph begin
  Ob::Data
  Hom::Data
  ob::Attr(V,Ob)
  hom::Attr(E,Hom)
end

Since a free diagram is supposed to be a functor out of a freely generated category, it would be better to have:

@present TheoryFreeDiagram <: TheoryGraph begin
  Ob::Data
  Hom::Data
  dom::DataHom(Hom,Ob)
  codom::DataHom(Hom,Ob)

  ob::Attr(V,Ob)
  hom::Attr(E,Hom)

  compose(src, ob) == compose(hom, dom)
  compose(tgt, ob) == compose(hom, codom)
end

The intended interpretation is that whatever Julia types instantiate Ob and Hom should have methods dom(::Hom)::Ob and codom(::Hom)::Ob and then the instance data should satisfy the two equations.

At least to start with, this feature would be for documentation/specification purposes and would not provide any new functionality. Thoughts on this, @olynch?

[olynch]

Yeah, we already don't really enforce the equations, so I think it's generally fine to have things in the schema that don't come into the presentation.

Julia just doesn't have the right type system for everything we would want to do with it, but... eh, we make do.

One way of interpreting this would be to say that Data is a category enriched over method-sets (which are sets decorated by julia methods), and JType is the category of julia types and julia functions, also enriched over method-sets (i.e. each function between two types is an implementation of some method). Then K : Data -> JType is a method-set enriched functor.

This has the advantage of clarifying that the "data" of K is exactly the choice of types for each object of K; given this choice of types, the choice of functions in JType is uniquely specified by the method-preserving property.

[olynch]

Now that I think of it, can we enrich over arbitrary acsets? :eyes: