A syntax for higher inductive-inductive types

[András Kovács]

Dear all,

We have a draft titled "A Syntax for Higher Inductive-Inductive Types" which may be of interest to you. There's also an Agda formalization, and a Haskell implementation of a HIIT type/positivity checker and eliminator-generator which you can play around with. Here are a number of examples.

The main idea is to describe HIIT-s as contexts in a "domain specific" type theory. This type theory has a universe closed under identity types, and a function space restricted to small (i. e. contained in the universe) domain types, which enforces strict positivity. Then, one can compute types of algebras, induction methods and eliminators/beta rules by taking various models of this type theory. Non-closed HIITs and infinitary constructors can be also represented by additional function spaces, with domain types built from an "external" non-inductive context. We do not say anything about existence or semantics of specified types yet.

András Kovács

Ambrus Kaposi