The existential completion

TL;DR

This paper investigates the existential completion of primary doctrines, establishing its properties, including lax-idempotency of the associated 2-monad, and explores its implications for elementary and exact doctrines.

Contribution

It introduces the existential completion for primary doctrines, proves the lax-idempotency of the related 2-monad, and extends the notion of exact completion to elementary doctrines.

Findings

The 2-monad from the existential completion is lax-idempotent.

The 2-category of existential doctrines is isomorphic to the category of algebras for this 2-monad.

The existential completion of an elementary doctrine remains elementary.

Abstract

We determine the existential completion of a primary doctrine, and we prove that the 2-monad obtained from it is lax-idempotent, and that the 2-category of existential doctrines is isomorphic to the 2-category of algebras for this 2-monad. We also show that the existential completion of an elementary doctrine is again elementary. Finally we extend the notion of exact completion of an elementary existential doctrine to an arbitrary elementary doctrine.