A co-free construction for elementary doctrines

TL;DR

This paper introduces a co-free construction that enhances primary doctrines with elementary structure, preserving logical operations and comprehensions, and ensuring extensional entailment in implicational doctrines.

Contribution

It presents a novel co-free construction method that adds elementary structure to primary doctrines while preserving existing logical features.

Findings

Preserves comprehensions and logical operations

Maps first-order theories into equality-formulated theories

Enforces extensional entailment in implicational doctrines

Abstract

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.