Till innehåll på sidan

Jacopo Emmenegger: W-types in setoids

Tid: On 2018-11-28 kl 10.00 - 11.45

Plats: Room 16, building 5 kräftriket, Department of Mathematics, Stockholm University 

Medverkande: Jacopo Emmenegger

Exportera till kalender

Abstract: W-types are very general inductive types and, from a set-theoretic perspective, can be seen as representatives of well orders. Moerdijk and Palmgren identified a semantic analogue in initial algebras of polynomial endofunctors. Current arguments to obtain such initial algebras in categories of equivalence relations rely on assumptions like Uniqueness of Identity Proofs or on constructions that involve recursion into a universe.

We present a new argument, verified in Coq, that instead uses a generalisation of W-types in the underlying type theory, known as dependent W-types. These type constructors endow the theory with enough expressive power to characterise maps obtained by initiality as those maps satisfying a certain recursive equation. In addition, not relying on any extensionality principle nor on existence of universes, this argument is valid in a fully intensional theory and it is suitable for being formulated in rather weak category-theoretic settings.