The (Pi,lambda)-structures on the C-systems defined by universe categories

MaRDI QIDQ2963471zbMATH OpenFDO

Authors Vladimir Voevodsky

Publication date 14 February 2017

Full work available at URL https://arxiv.org/abs/1706.03618, http://www.emis.de/journals/TAC/volumes/32/4/32-04abs.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 categorydependent productproduct of families of typesuniverse 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)

Abstract: We define the notion of a (P,P-tilde)-structure on a universe p in a locally cartesian closed category category C with a binary product structure and construct a (Pi,lambda)-structure on the C-systems CC(C,p) from a (P,P-tilde)-structure on p. We then define homomorphisms of C-systems with (Pi,lambda)-structures and functors of universe categories with (P,P-tilde)-structures and show that our construction is functorial relative to these definitions.

Recommendations

• Products of families of types and (Pi,lambda)-structures on C-systems
• Categories of (ℓ, ℛ)-systems
• scientific article; zbMATH DE number 4021100
• scientific article; zbMATH DE number 1092283
• Cubical \((\omega, p)\)-categories
• scientific article; zbMATH DE number 663785
• On universal categories of coalgebras
• Towards a characterization of universal categories
• C^* -Categories
• On the Existence of Categorical Universal Coverings

Cites work

• scientific article; zbMATH DE number 226803 (Why is no real title available?)
• A C-system defined by a universe category
• C-systems defined by universe categories: presheaves
• Generalized algebraic theories and contextual categories
• Locally cartesian closed categories and type theory
• Products of families of types and (Pi,lambda)-structures on C-systems
• Subsystems and regular quotients of C-systems
• The biequivalence of locally Cartesian closed categories and Martin-Löf type theories

Cited in

(12)

• Martin-Löf identity types in C-systems
• Lawvere theories and C-systems
• The étale cohomology of the general linear group over a finite field and the Dickson algebra
• The simplicial model of univalent foundations (after Voevodsky)
• Construction of the circle in \textit{UniMath}
• The Interpretation Lifting Theorem for C-Systems
• C-system of a module over a \(Jf\)-relative monad
• C-systems defined by universe categories: presheaves
• Vladimir Aleksandrovich Voevodsky
• Products of families of types and (Pi,lambda)-structures on C-systems
• A C-system defined by a universe category
• An introduction to univalent foundations for mathematicians

Describes a project that uses

Uses Software

• GitHub
• UniMath

This page was built for publication: The (Pi,lambda)-structures on the C-systems defined by universe categories

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