The AQL tool (http://categoricaldata.net/aql.html) implements David Spivak's schemas-as-categories idea in working software. One of AQL's built-in examples is roughly the example from this thread:


schema S = literal {
entities
Employee
Department
foreign_keys
manager : Employee -> Employee
worksIn : Employee -> Department
secretary : Department -> Employee
path_equations
manager.worksIn = worksIn
secretary.worksIn = id_Department
attributes
first last : Employee -> string
name : Department -> string
}


instance I = literal : S {
generators
a b c : Employee
m s : Department
equations
first(a) = Al
first(b) = Bob last(b) = Bo
first(c) = Carl
name(m) = Math name(s) = CS
age(a) = age(c)
manager(a) = b manager(b) = b manager(c) = c
worksIn(a) = m worksIn(b) = m worksIn(c) = s
secretary(s) = c secretary(m) = b
secretary(worksIn(a)) = manager(a)
worksIn(a) = worksIn(manager(a))
}

AQL's connections to functional programming and database theory are significant and are discussed in a series of papers available at http://categoricaldata.net/fql.html . For example, the query language obtained from delta/sigma/pi can be written using 'SQL-ish' notation, and reasoning about schemas and functors requires use of automated theorem proving methods (e.g., Knuth-Bendix completion).

The AQL project is currently recruiting people who have backgrounds in
- category theory
- type theory / functional programming
- automated theorem proving
- database internals / SQL at scale

If you are interested in participating, please let me know (ryan@catinf.com)