I think I can answer my own question: it's enough to have conjunction, truth, and equations to get a complete semantics of lex categories. This really is just an exercise in categorical logic. Sorry for bothering everyone with it. We work over multi-sorted type theory. The basic judgments are 1) term t has type B in typing context x_1:A_1,...,x_n:A_n: x_1:A_1,...,x_n:A_n | t : B 2) phi is a formula in context x_1:A_1,...x_n:A_n x_1:A_1,...,x_n:A_n | phi 3) assumptions psi_1,...,psi_k logically entail phi: x_1:A_1,...,x_n:A_n | psi_1,...,psi_k |- phi Formulas are built from equality, truth, and conjunction. The syntactic model is built as follows: - OBJECTS are formulas in contexts x_1:A_1, ..., x_n:A_n | phi where A_i are types, x_i are distinct variables, and phi is a formula built from truth T, conjunction and equations. The variables appearing in phi must be listed in the context. Two formulas in contexts which only differ in the names of variables are considered equal. - MORPHISMS: let Gamma be the context x_1:A_1, ..., x_n:A_n and Delta the context y_1:B_1, ..., y_m:B_m. A morphism t Gamma|phi -------> Delta|psi is an m-tuple of terms t = <t_1, ..., t_m>, where the type of t_i in context Gamma is B_i, written as Gamma | t_i : B_i, such that the following is provable: Gamma | phi and (y_1 = t_1) and ... and (y_m = t_m) |- psi In words, the assumption phi together with the assumptions y_1 = t_1, ..., y_m = t_m logically entail psi. Composition is defined by substitution. The identity morphism on Gamma|phi is the tuple <x_1,...,x_n>. Morphisms are quotiented modulo provable equality. More precisely, morphisms t Gamma|phi -------> Delta|psi and s Gamma|phi -------> Delta|psi are considered provably equal if the following entailment is provable, for every i = 1,...,m: Gamma | phi |- t_i = s_i This probably does the job, i.e., the syntactic model is a category with finite limits and is universal such category. The product of objects Gamma | phi and Delta | psi is the product Gamma, Delta | phi and psi where the contexts Gamma and Delta are presumed to list disjoint sets of variables (this can always be achieved by renaming). The equalizer of ---t---> Gamma|phi Delta|psi ---s---> is the object Gamma | phi and (t_1 = s_1) and ... and (t_m = s_m) with the obvious inclusion into Gamma|phi. I think this does the job. Andrej 18-Dec-2002 11:59:17 -0400,1421;000000000001-00000000