C-systems defined by universe categories: presheaves

MaRDI QIDQ2963470zbMATH OpenFDO

Authors Vladimir Voevodsky

Publication date 14 February 2017

Full work available at URL https://arxiv.org/abs/1706.03620, http://www.emis.de/journals/TAC/volumes/32/3/32-03abs.html

IPFS File on IPFS (Hint: this is only the Hash - if you get a timeout, this file is not available on our server.)

zbMATH Keywords

type theorycontextual category

Mathematics Subject Classification ID

Metamathematics of constructive systems (03F50) Categorical semantics of formal languages (18C50) Closed categories (closed monoidal and Cartesian closed categories, etc.) (18D15) Type theory (03B38)

Abstract: The main result of this paper may be stated as a construction of "almost representations" for the canonical presheaves of object extensions of length n on the C-systems defined by locally cartesian closed universe categories with binary product structures and the study of the behavior of these "almost representations" with respect to the universe category functors. In addition, we study a number of constructions on presheaves on C-systems and on universe categories that are used in the proofs of our main results, but are expected to have other applications as well.

Recommendations

• A C-system defined by a universe category
• Systems on universe spaces
• The (Pi,lambda)-structures on the C-systems defined by universe categories
• CATEGORICAL APPROACH TO GENERAL SYSTEMS THEORY
• scientific article; zbMATH DE number 889968
• Publication:4862450
• Categories and orbispaces
• scientific article; zbMATH DE number 2019859
• Revisiting the categorical approach to systems
• Categoricity and universal classes

Cites work

• scientific article; zbMATH DE number 195199 (Why is no real title available?)
• scientific article; zbMATH DE number 226803 (Why is no real title available?)
• A C-system defined by a universe category
• Generalized algebraic theories and contextual categories
• Products of families of types and (Pi,lambda)-structures on C-systems
• Subsystems and regular quotients of C-systems
• The (Pi,lambda)-structures on the C-systems defined by universe categories
• Types for Proofs and Programs

Cited in

(11)

• Presheaves as configured specifications
• Martin-Löf identity types in C-systems
• Construction of the circle in \textit{UniMath}
• The mysterious story of square ice, piles of cubes, and bijections
• The Interpretation Lifting Theorem for C-Systems
• C-system of a module over a \(Jf\)-relative monad
• The (Pi,lambda)-structures on the C-systems defined by universe categories
• Vladimir Aleksandrovich Voevodsky
• A C-system defined by a universe category
• An introduction to univalent foundations for mathematicians
• The first bijective proof of the refined ASM theorem

This page was built for publication: C-systems defined by universe categories: presheaves

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2963470)