The extensive completion of a distributive category (Q2761574)

The main result of this paper is the universal construction of an extensive category \({\mathcal D}_{\text{ex}}\) with products for each distributive category \({\mathcal D}\), together with a functor \({\mathcal D}\to {\mathcal D}_{\text{ex}}\) preserving finite products and finite coproducts. Formally speaking, the authors construct a left biadjoint to the inclusion of \({\mathfrak{Ext}}_{\mathfrak{pr}}\) into \(\mathfrak{Dist}\), where \(\mathfrak{Dist}\) is the 2-category of distributive categories, distributive functors and natural transformations, and \({\mathfrak{Ext}}_{\text{pr}}\) denotes its full sub-2-category of extensive ones.