C-systems defined by universe categories: presheaves

zbMATH Open1453.03067arXiv1706.03620MaRDI QIDQ2963470FDOQ2963470

Authors: Vladimir Voevodsky 

Publication date: 14 February 2017

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.

Full work available at URL: https://arxiv.org/abs/1706.03620

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

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

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)

Cites Work

• Title not available (Why is that?)
• Title not available (Why is that?)
• Generalized algebraic theories and contextual categories
• Types for Proofs and Programs
• The (Pi,lambda)-structures on the C-systems defined by universe categories
• Products of families of types and (Pi,lambda)-structures on C-systems
• Subsystems and regular quotients of C-systems
• A C-system defined by a universe category

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)