  We provide a co-free construction which adds elementary structure to a
primary doctrine. We show that the construction preserves comprehensions and
all the logical operations which are in the starting doctrine, in the sense
that it maps a first order many-sorted theory into a the same theory formulated
with equality. As a corollary it forces an implicational doctrine to have an
extentional entailment.
