6533b827fe1ef96bd1286817
RESEARCH PRODUCT
Wellfounded Trees and Dependent Polynomial Functors
Nicola GambinoMartin Hylandsubject
Class (set theory)Pure mathematicsCartesian closed categoryFunctorType theoryMathematics::Category TheoryComputer Science::Logic in Computer ScienceWellfounded trees locally cartesian closed categories categorical logicTree (set theory)PrewellorderingCategory theoryForgetful functorMathematicsdescription
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.
| year | journal | country | edition | language |
|---|---|---|---|---|
| 2004-01-01 |