A General Framework for the Semantics of Type Theory

Taichi Uemura

A General Framework for the Semantics of Type Theory

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 1904.04097 v3 pith:F63YEAPF submitted 2019-04-08 math.CT cs.LOmath.LO

Taichi Uemura This is my paper · ORCID

classification math.CTcs.LOmath.LO

keywords typetheorysemanticscategoryeverymodeltheoriesabstract

verification ladder T0 review T1 audit T2 compute T3 formal

0 comments

read the original abstract

We propose an abstract notion of a type theory to unify the semantics of various type theories including Martin-L\"{o}f type theory, two-level type theory and cubical type theory. We establish basic results in the semantics of type theory: every type theory has a bi-initial model; every model of a type theory has its internal language; the category of theories over a type theory is bi-equivalent to a full sub-2-category of the 2-category of models of the type theory.

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

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