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.
Lingua originale | English |
---|---|
Numero di pagine | 15 |
Stato di pubblicazione | Published - 2004 |
All Science Journal Classification (ASJC) codes
- ???subjectarea.asjc.2600.2614???
- ???subjectarea.asjc.1700.1700???