Stefania Damato: Initial Algebra Semantics for QIITs using Containers

Abstract

It is well known that ordinary inductive types and inductive families can be described semantically as initial algebras of container functors and indexed container functors respectively. In this talk, I will present ongoing work on a similar initial algebra semantics for the more general class of quotient inductive-inductive types (QIITs). A semantic framework for QIITs has already been developed in [1]. Our proposed approach is to introduce restrictions to this framework, including restricting the functors in this framework to generalised containers, to carve out those QIIT specifications that are guaranteed to have an initial algebra.

[1] : Altenkirch, Thorsten & Capriotti, Paolo & Dijkstra, Gabe & Kraus, Nicolai & Forsberg, Fredrik. (2018). Quotient Inductive-Inductive Types. 10.1007/978-3-319-89366-2_16.