The (Pi,lambda)-structures on the C-systems defined by universe categories
From MaRDI portal
Publication:2963471
zbMATH Open1383.03056arXiv1706.03618MaRDI QIDQ2963471FDOQ2963471
Publication date: 14 February 2017
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.
Full work available at URL: https://arxiv.org/abs/1706.03618
File on IPFS (Hint: this is only the Hash - if you get a timeout, this file is not available on our server.)
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
Metamathematics of constructive systems (03F50) Categorical semantics of formal languages (18C50) Closed categories (closed monoidal and Cartesian closed categories, etc.) (18D15)
Cites Work
- Title not available (Why is that?)
- 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
- A C-system defined by a universe category
- C-systems defined by universe categories: presheaves
- The biequivalence of locally cartesian closed categories and Martin-Löf type theories
Cited In (10)
- Martin-Löf identity types in 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
- An introduction to univalent foundations for mathematicians
Uses Software
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)
