A syntax for higher inductive-inductive types

["András Kovács" <"putta..."@gmail.com>]

[-- Attachment #1.1: Type: text/plain, Size: 1249 bytes --]

Dear all,

We have a draft titled "A Syntax for Higher Inductive-Inductive Types" 
<https://akaposi.github.io/hiit.pdf> which may be of interest to you. 
There's also an Agda formalization <https://bitbucket.org/akaposi/elims>, 
and a Haskell implementation <https://bitbucket.org/akaposi/elims> of a 
HIIT type/positivity checker and eliminator-generator which you can play 
around with. Here 
<https://bitbucket.org/akaposi/elims/src/0fd2d3e8226e08757e2ab460a5b5966e6a6fb4c4/haskell/elims-demo/examples/?at=master> 
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

[-- Attachment #1.2: Type: text/html, Size: 1395 bytes --]