Pith. sign in

REVIEW 1 cited by

B-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 1410.5389 v1 pith:4CR2HX73 submitted 2014-10-20 math.LO math.CT

Vladimir Voevodsky This is my paper · ORCID
classification math.LOmath.CT
keywords theoryb-systemscategoriesalgebraicc-systemsconstructivelycontextualequivalent
verification ladder T0 review T1 audit T2 compute T3 formal
0 comments
read the original abstract

B-systems are algebras (models) of an essentially algebraic theory that is expected to be constructively equivalent to the essentially algebraic theory of C-systems which is, in turn, constructively equivalent to the theory of contextual categories. The theory of B-systems is closer in its form to the structures directly modeled by contexts and typing judgements of (dependent) type theories and further away from categories than contextual categories and C-systems.

Discussion (0). Continue with ORCID to comment.

Forward citations

Cited by 1 Pith paper

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

  1. 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