We set out to study the consequences of the assumption of types of wellfounded trees in dependent type theories. We do so by in- vestigating the categorical notion of wellfounded tree introduced in [16]. Our main result shows that wellfounded trees allow us to define initial algebras for a wide class of endofunctors on locally cartesian closed cat- egories.
GAMBINO, N., HYLAND, M. (2004). Wellfounded Trees and Dependent Polynomial Functors. In Types 2003. Springer [10.1007/978-3-540-24849-1_14].
Wellfounded Trees and Dependent Polynomial Functors
GAMBINO, Nicola;
2004-01-01
Abstract
We set out to study the consequences of the assumption of types of wellfounded trees in dependent type theories. We do so by in- vestigating the categorical notion of wellfounded tree introduced in [16]. Our main result shows that wellfounded trees allow us to define initial algebras for a wide class of endofunctors on locally cartesian closed cat- egories.
File in questo prodotto:
Non ci sono file associati a questo prodotto.
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
