Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Biased elementary doctrines and quotient completions

Cipriano Junior Cioffo

TL;DR

This work extends Lawvere-style doctrines to categories with weak finite products by introducing biased elementary doctrines and two main constructions: a strictification that yields an elementary doctrine on the finite product completion, and a biased quotient completion that generalizes both the elementary quotient completion and the exact completion for categories with weak finite limits. It develops the notion of proof-irrelevant elements to manage equalities in the presence of weak products, defines a coherent quotient construction with a universal property via left-covering-like morphisms, and shows that slice doctrines and quotient completions interact well within this biased framework. The approach recovers known examples (e.g., Set_G, setoids in Minimalist Foundation) as biased completions and provides a unified account for families of setoids and related semantic models, while linking to results on local cartesian closure and exponentials in quotient contexts. The framework thus generalizes exact and elementary quotient completions to new domains and offers a robust tool for studying quotient models arising from type theory and related logics.

Abstract

In this work, we fill the gap between the elementary quotient completion introduced by Maietti and Rosolini and the exact completion of a category with weak finite limits, as described by Carboni and Vitale. To achieve this, we generalize Lawvere's elementary doctrines to apply to categories with weak finite products, referring to these structures as biased elementary doctrines. We present two main constructions: the first, called strictification, produces an elementary doctrine from a biased one, while the second is an extension of the elementary quotient completion that generalizes the exact completion of a category with weak finite limits, even when weak finite products are involved.

Biased elementary doctrines and quotient completions

TL;DR

This work extends Lawvere-style doctrines to categories with weak finite products by introducing biased elementary doctrines and two main constructions: a strictification that yields an elementary doctrine on the finite product completion, and a biased quotient completion that generalizes both the elementary quotient completion and the exact completion for categories with weak finite limits. It develops the notion of proof-irrelevant elements to manage equalities in the presence of weak products, defines a coherent quotient construction with a universal property via left-covering-like morphisms, and shows that slice doctrines and quotient completions interact well within this biased framework. The approach recovers known examples (e.g., Set_G, setoids in Minimalist Foundation) as biased completions and provides a unified account for families of setoids and related semantic models, while linking to results on local cartesian closure and exponentials in quotient contexts. The framework thus generalizes exact and elementary quotient completions to new domains and offers a robust tool for studying quotient models arising from type theory and related logics.

Abstract

In this work, we fill the gap between the elementary quotient completion introduced by Maietti and Rosolini and the exact completion of a category with weak finite limits, as described by Carboni and Vitale. To achieve this, we generalize Lawvere's elementary doctrines to apply to categories with weak finite products, referring to these structures as biased elementary doctrines. We present two main constructions: the first, called strictification, produces an elementary doctrine from a biased one, while the second is an extension of the elementary quotient completion that generalizes the exact completion of a category with weak finite limits, even when weak finite products are involved.
Paper Structure (7 sections, 21 theorems, 71 equations)

This paper contains 7 sections, 21 theorems, 71 equations.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Biased elementary doctrines
  4. Proof-irrelevant elements
  5. Strictification
  6. Quotient completion
  7. Concluding remarks

Key Result

Proposition 2.4

Let $\mathscr{C}$ be a category with strict finite products. A primary doctrine $\mathsf{P}:\mathscr{C}^{\operatorname{op}}\to \mathsf{InfSL}$ is elementary if and only if for every object $X\in\mathscr{C}$, there exists an element $\delta_X\in \mathsf{P}(X\times X)$ such that: where the arrows $p_i$, for $1\le i\le 4$, are the projections of the product $X\times Y\times X\times Y$. ∎

Theorems & Definitions (84)

  • Definition 2.1
  • Definition 2.2
  • Definition 2.3
  • Proposition 2.4
  • Definition 2.5
  • Definition 2.6
  • Definition 2.7
  • Definition 2.8
  • Definition 2.9
  • Definition 2.11
  • ...and 74 more