C-systems were defined by Cartmell as models of generalized algebraic theories. B-systems were defined by Voevodsky in his quest to formulate and prove an initiality conjecture for type theories. They play a crucial role in Voevodsky’s construction of a syntactic C-system from a term monad. In this work, we construct an equivalence between the category of C-systems and the category of B-systems, thus proving a conjecture by Voevodsky.
B-SYSTEMS AND C-SYSTEMS ARE EQUIVALENT / Ahrens, B., Emmenegger, J., Randall North, P., Rijke, E.. - In: THE JOURNAL OF SYMBOLIC LOGIC. - ISSN 0022-4812. - 89:(2023), pp. 1513-1521. [10.1017/jsl.2023.41]
B-SYSTEMS AND C-SYSTEMS ARE EQUIVALENT
JACOPO EMMENEGGER;
2023
Abstract
C-systems were defined by Cartmell as models of generalized algebraic theories. B-systems were defined by Voevodsky in his quest to formulate and prove an initiality conjecture for type theories. They play a crucial role in Voevodsky’s construction of a syntactic C-system from a term monad. In this work, we construct an equivalence between the category of C-systems and the category of B-systems, thus proving a conjecture by Voevodsky.| File | Dimensione | Formato | |
|---|---|---|---|
|
Arhens_B-systems_2024.pdf
accesso aperto
Tipologia:
Versione editoriale (versione pubblicata con il layout dell'editore)
Licenza:
Creative commons
Dimensione
192.96 kB
Formato
Adobe PDF
|
192.96 kB | Adobe PDF |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
