These agda files attempt to reduce inductive-inductive types to inductive Families. They are supposed to be checked using Agda version 2.5.4.1. Later versions' REWRITE pragmas might not be compatible with the formalization anymore, sorry.

Contains the syntax for closed inductive-inductive types

Contains the syntax for indexed inductive types with contexts for sort (Scon) and for point constructors (Con).

Contains the Set interpretation of the syntax described in IF.agda, describing algebras of indexed inductive types.

Contains the model for the indexed inductive types which describes morphisms.

Contains displayed algebras of indexed inductive types. These algebras depend on an algebra as described in IFA.agda.

Contains the indexed inductive type interpretation for the section of the aforementioned displayed algebras.

Shows the existence of inductive families given the internalization of the syntax as given in IF.agda.

Contains the definitions on how to obtain the the erasure E, the wellformedness w, the eliminator relation R and the initial object Sg for inductive-inductive types.

Encapsulates the previous files by assuming the existence of indexed inductive types and deriving the existence of inductive-inductive types.

The types of natural numbers as a test case.

The type of vectors as a test case.

The example of contexts and types of a type theoretical syntax as a test case.