Subsystems and regular quotients of C-systems
From MaRDI portal
Publication:2990151
DOI10.1090/conm/658/13124zbMath1452.03040arXiv1406.7413OpenAlexW1755504862MaRDI QIDQ2990151
Publication date: 29 July 2016
Published in: A Panorama of Mathematics: Pure and Applied (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/1406.7413
Other algebras related to logic (03G25) Metamathematics of constructive systems (03F50) Abstract deductive systems (03B22) Type theory (03B38)
Related Items (14)
Categorical structures for type theory in univalent foundations ⋮ Vladimir Aleksandrovich Voevodsky ⋮ On generalized algebraic theories and categories with families ⋮ The Interpretation Lifting Theorem for C-Systems ⋮ Martin-Löf identity types in C-systems ⋮ C-system of a module over a \(Jf\)-relative monad ⋮ An introduction to univalent foundations for mathematicians ⋮ Unnamed Item ⋮ The homotopy theory of type theories ⋮ Construction of the circle in \textit{UniMath} ⋮ The simplicial model of univalent foundations (after Voevodsky) ⋮ Lawvere theories and C-systems ⋮ C-systems defined by universe categories: presheaves ⋮ The (Pi,lambda)-structures on the C-systems defined by universe categories
This page was built for publication: Subsystems and regular quotients of C-systems
