Dear all,
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