Can you define schema describing a category?

[Kamil D]

Greetings,

Defining a schema for a graph is obvious, but can you define a schema for a category?

When trying to do this, I find myself needing to use a pullback to define an object representing permissible arrow combinations, but I don't suppose limits are available in a schema. Even if they were available, the instance functor is not guaranteed to preserve them.

Regards,

Kamil

[Ryan Wisnesky]

You are correct: categories cannot be equationally axiomatized (their models are of an “essentially algebraic theory”, not an “algebraic” theory).  However, CQL does allow one to define such theories, basically by using a fragment of first-order logic that does indeed include pullbacks:

schema cat = literal : empty {

entities

Ob Mor Pair

foreign_keys

id: Ob -> Mor

dom: Mor -> Ob

cod: Mor -> Ob

Fst: Pair -> Mor

Snd: Pair -> Mor

comp: Pair -> Mor

path_equations

Ob.id.dom = Ob

Ob.id.cod = Ob

Pair.Fst.dom = Pair.comp.dom

Pair.Fst.cod = Pair.Snd.dom

Pair.Snd.cod = Pair.comp.cod

options

}

constraints theEDs = literal : cat {

#every composable pair gives a Pair

forall f g:Mor

where f.cod=g.dom ->

  exists unique fg:Pair

  where fg.Fst=f fg.Snd=g

#left unitality

forall fid:Pair

where fid.Fst.cod.id = fid.Snd

->

where fid.comp = fid.Fst

#right unitality

forall idf:Pair

where idf.Snd.dom.id = idf.Fst

->

where idf.comp = idf.Snd

#associativity

  forall fg gh fgThenh fThengh: Pair

  where

  fg.Snd = gh.Fst

  fgThenh.Fst = fg.comp

  fgThenh.Snd = gh.Snd

  fThengh.Fst = fg.Fst

  fThengh.Snd = gh.comp

  ->

  where fgThenh.comp = fThengh.comp

}

--
You received this message because you are subscribed to the Google Groups "Categorical Data" group.
To unsubscribe from this group and stop receiving emails from it, send an email to categoricalda...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/categoricaldata/49415019-6758-4cac-adbe-97ae2a1a6359n%40googlegroups.com.

[Kamil D]

The constraints aren't guaranteed to be preserved by transformations, right? I see them used as instance validators and with chase operator for closing the data in the instance to conform to the constraints.

[Ryan Wisnesky]

Correct, constraints are not guaranteed to be preserved by delta/sigma/pi.  However, if you have Q : C -> D a CQL query, and phi a C-constraint, and psi a D-constraint, then you do have: 

phi entails coeval_Q(psi) 

-----------------------------------------------------------------------

For every I that satisfies phi, eval_C(I) satisfies psi  

In fact, we have a product that checks this condition using automated theorem proving techniques.

To view this discussion on the web visit https://groups.google.com/d/msgid/categoricaldata/3214a8fd-cc05-4cc0-ba89-0a69277aa3fen%40googlegroups.com.

[Kamil D]

What's coeval_Q?

[Ryan Wisnesky]

CQL includes both eval and coeval as keywords: given a CQL query Q : S -> T, eval transforms S-instances to T-instances and coeval transforms T-instances to S-instances - it is the left adjoint to eval.  It’s described in various math papers.

To view this discussion on the web visit https://groups.google.com/d/msgid/categoricaldata/a6d69c63-7e47-4ba1-917d-877a7e442d58n%40googlegroups.com.