These agda files are a formalization of the Paper with the above title. They are supposed to be checked using Agda version 2.5.4.1. Later versions of Agda might brake the rewrite pragmas we used.
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.
Lists some of the Examples presented in the paper: natural numbers, parity, and vectors.