On algebraically exact categories and essential localizations of varieties spaces Algebraically exact categories have been introduced by Adamek, Lawvere and Rosicky as an equational hull of the 2-category of all varieties of finitary algebras. Our main result is the following representation theorem for algebraically exact categories:

This theorem is a further step in the non-additive generalization of some fundamental theorems in commutative algebra: In a similar way, we also characterize essential localizations of presheaf categories.
This is joint work with J. Adamek and J. Rosicky.

Arity Polymorphism and Dependent Types In polytypic programming one would like to define combinators, such as map, which operate on datatype constructors of any arity. However, it is rather problematic to devise a type system that can express this form of polymorphism. In a calculus like Functorial ML, instead of having one combinator map, one has a family of combinators map_n parametrized over natural numbers, while in a system like PolyP there are restriction on the arity of datatype constructors. The most natural typing for the map combinator would be

Forall n:N. Forall F:Functor(n). Forall X,Y:Type^n.
  [ Forall i:n. X_i -> Y_i ] -> F(X) -> F(Y)
where n ranges over arities (say the numbers), F over functors of arity n, X and Y over n-tuples of types, and i over indices for arity n (e.g. the predecessors of n). We propose a type system with a limited form of dependent types and inductive types, which supports arity polymorphism.