Pith. sign in

REVIEW 2 cited by

Biased elementary doctrines and quotient completions

Not yet reviewed by Pith; the record is open.

This paper has not been read by Pith yet. Machine review is queued; the pith claim, tier, and objections will appear here once it completes.

SPECIMEN: schema-true, not a live event

T0 review · schema-true

One-sentence machine reading of the paper's core claim.

pith:XXXXXXXX · record.json · timestamp

arxiv 2304.03066 v2 pith:KIZSQ2J6 submitted 2023-04-06 math.CT math.LO

classification math.CTmath.LO
keywords elementarycompletionfiniteweakbiaseddoctrinesquotientcategory
verification ladder T0 review T1 audit T2 compute T3 formal
0 comments
read the original 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.

Discussion (0). Continue with ORCID to comment.

Forward citations

Cited by 2 Pith papers

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score. Full citation record

  1. The Relational Quotient Completion

    math.CT 2024-12 conditional novelty 7.0 of 10

    A new categorical framework, relational doctrines, yields universal quotient and extensionality completions that unify exact completion, setoids, and quantitative metric quotients.

  2. Fibred sets within a predicative and constructive effective topos

    math.LO 2024-11 conditional novelty 6.0 of 10

    The authors show that the predicative effective topos pEff carries a fibred structure of 'sets', whose fibres are locally cartesian closed list-arithmetic pretoposes with a small subobject classifier and formal Church...

Pith tools