Algebraic presentations of type dependency

DOI10.46298/LMCS-21(1:14)2025MaRDI QIDQ7016773zbMATH OpenFDO

Authors Benedikt Ahrens, Jacopo Emmenegger, Paige Randall North, Egbert Rijke

Publication date 6 March 2025

Published in Logical Methods in Computer Science (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.46298/LMCS-21(1:14)2025

Mathematics Subject Classification ID

Type theory (03B38) Categories of fibrations, relations to (K)-theory, relations to type theory (18N45)

Cites work

• scientific article; zbMATH DE number 1216133 (Why is no real title available?)
• scientific article; zbMATH DE number 1241699 (Why is no real title available?)
• scientific article; zbMATH DE number 1289305 (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
• B-systems and C-systems are equivalent
• C-system of a module over a \(Jf\)-relative monad
• C-systems defined by universe categories: presheaves
• Categorical structures for type theory in univalent foundations
• Combinatorial structure of type dependency
• Generalized algebraic theories and contextual categories
• Identity types and weak factorization systems in Cauchy complete categories
• Internal type theory
• Lawvere theories and C-systems
• Martin-Löf identity types in C-systems
• Natural models of homotopy type theory
• 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
• The simplicial model of univalent foundations (after Voevodsky)
• Univalence for inverse diagrams and homotopy canonicity

This page was built for publication: Algebraic presentations of type dependency

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