A C-system defined by a universe category
From MaRDI portal
Publication:3456330
zbMath1436.03311arXiv1409.7925MaRDI QIDQ3456330
Publication date: 14 December 2015
Full work available at URL: https://arxiv.org/abs/1409.7925
Categorical logic, topoi (03G30) Metamathematics of constructive systems (03F50) Categories and theories (18C99) Type theory (03B38)
Related Items (15)
Categorical structures for type theory in univalent foundations ⋮ Vladimir Aleksandrovich Voevodsky ⋮ The Interpretation Lifting Theorem for C-Systems ⋮ Martin-Löf identity types in C-systems ⋮ On the ∞$\infty$‐topos semantics of homotopy type theory ⋮ C-system of a module over a \(Jf\)-relative monad ⋮ An introduction to univalent foundations for mathematicians ⋮ 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 ⋮ Modal dependent type theory and dependent right adjoints ⋮ From signatures to monads in \textsf{UniMath} ⋮ 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: A C-system defined by a universe category
