This repository contains draft sources and formalizations for the paper "Signatures and Induction Principles for Higher Inductive-Inductive Types", by Ambrus Kaposi and András Kovács. This paper is an extended version of the FSCD 2018 paper by the same authors, titled "A Syntax for Higher Inductive-Inductive Types", which has additional materials at https://bitbucket.org/akaposi/elims.
You can find the formalization in the formalization folder. You can find a Haskell implementation in the elims-demo folder.