Pith. sign in

REVIEW 2 cited by

Subsystems and regular quotients of C-systems

Not yet reviewed by Pith; the record is open.

Re-run · record.json Download PDF Read on arXiv ↗

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 1406.7413 v3 pith:YQ6T3TUY submitted 2014-06-28 math.LO

Vladimir Voevodsky This is my paper · ORCID
classification math.LO
keywords c-systemssub-objectscasequotient-objectsquotientsregularversionauthor
verification ladder T0 review T1 audit T2 compute T3 formal
0 comments
read the original abstract

C-systems were introduced by J. Cartmell under the name "contextual categories". In this note we study sub-objects and quotient-objects of C-systems. In the case of the sub-objects we consider all sub-objects while in the case of the quotient-objects only {\em regular} quotients that in particular have the property that the corresponding projection morphism is surjective both on objects and on morphisms. It is one of several short papers based on the material of the "Notes on Type Systems" by the same author. This version is essentially identical with the version published in Contemporary Mathematics n.658.

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. A monoidal category of dependently sorted algebraic theories II: categorical aspects

    math.CT 2026-05 unverdicted novelty 6.0 of 10

    Constructs the exponential A^B and proves existence of tensor A ⊗ B on contextual categories such that bimorphisms correspond to morphisms from the tensor, extending to a closed symmetric monoidal structure on Cont.

  2. Comparing semantic frameworks for dependently-sorted algebraic theories

    math.CT 2024-12 conditional novelty 5.0 of 10

    Nearly every categorical model of dependent type theory embeds as a usually full sub-2-category of comprehension categories, with each model distinguished by which maps its comprehension functor represents.

Pith tools