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
JACOPO EMMENEGGER;
2023-01-01
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 in questo prodotto:
| File | Dimensione | Formato | |
|---|---|---|---|
|
b-systems-and-c-systems-are-equivalent.pdf
accesso aperto
Descrizione: Articolo
Tipologia:
Documento in versione editoriale
Dimensione
192.96 kB
Formato
Adobe PDF
|
192.96 kB | Adobe PDF | Visualizza/Apri |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
