A categorical semantics for inductive-inductive definitions

Tools

Altenkirch, Thorsten and Morris, Peter and Nordvall Forsberg, Fredrik and Setzer, Anton; Corradini, Andrea and Klin, Bartek and Cîrstea, Corina, eds. (2011) A categorical semantics for inductive-inductive definitions. In: Algebra and Coalgebra in Computer Science. Lecture Notes in Computer Science . Springer Berlin/Heidelberg, GBR, pp. 70-84. ISBN 9783642229435 (https://doi.org/10.1007/978-3-642-22944-2_6)

Full text not available in this repository.Request a copy

Abstract

Induction-induction is a principle for defining data types in Martin-Löf Type Theory. An inductive-inductive definition consists of a set A, together with an A-indexed family B : A → Set, where both A and B are inductively defined in such a way that the constructors for A can refer to B and vice versa. In addition, the constructors for B can refer to the constructors for A. We extend the usual initial algebra semantics for ordinary inductive data types to the inductive-inductive setting by considering dialgebras instead of ordinary algebras. This gives a new and compact formalisation of inductive-inductive definitions, which we prove is equivalent to the usual formulation with elimination rules.

ORCID iDs

Altenkirch, Thorsten, Morris, Peter, Nordvall Forsberg, Fredrik ORCID logoORCID: https://orcid.org/0000-0001-6157-9288 and Setzer, Anton; Corradini, Andrea, Klin, Bartek and Cîrstea, Corina
CORE (COnnecting REpositories)