**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:

*a cocomplete category is algebraically exact and has a regular generator iff it is an essential localization of a variety.*

- Lawvere characterization of varieties is the non-additive extension of the Gabriel-Mitchell characterization of module categories;
- Popesco-Gabriel representation of Grothendieck categories has been extended to a non-additive context using the exact completion of a weakly left exact category;
- our main result is the non-additive generalization of Roos characterization of essential localizations of module 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.