> Just to answer your question,

I'm not sure what question you are answering.

I think you are answering "Couldn't schema be types like how Servant has routes as types?"

> the STLC forms a cartesian closed category, where the objects are types and the morphisms are terms. Similarly, the category of categories forms a cartesian closed category, where the objects are categories and the morphisms are functors. Similarly, AQL schemas form a cartesian closed category, where the objects are schemas (finitely presented categories) and the morphisms are schema mappings (morphisms of finitely presented categories). That is why it is natural to translate STLC types <-> categories and STLC terms <-> functors.

I am sorry, are you sure schemas really are the same as finitely presented categories? I thought they looked like this (taken from your website):

schema Schools = literal : Ty {
instituteOf : Person -> School
deptOf : Person -> Dept
biggestDept : School -> Dept
lastName : Person -> String
schoolName : School -> String
deptName : Dept -> String

> Under the above analogy, a concrete example of a finitely presented category that I'm not sure how to represent as a Haskell type/type family/etc but I know how to represent as a Coq type, is the presentation with two objects, A and B, two generating arrows f : A -> B and g : B -> A, and the equation f.g = id.

I feel like this is a tractable problem.

*How do we represent a two object finitely presented category in Haskell?*

Please check out Conal Elliot's paper [*Compiling to Categories* (2017)](http://conal.net/papers/compiling-to-categories/compiling-to-categories.pdf)

You appear to want a *Constrained Category* which Conal defines in ยง6.

It looks like you are heavily invested in Java, so I would understand if you weren't really interested in trying Haskell.