From mboxrd@z Thu Jan  1 00:00:00 1970
Date: Thu, 8 Feb 2018 03:23:32 -0800 (PST)
From: =?UTF-8?Q?Andr=C3=A1s_Kov=C3=A1cs?= <putta...@gmail.com>
To: Homotopy Type Theory <HomotopyT...@googlegroups.com>
Message-Id: <3214e47f-39f7-49d7-aa4a-ac6a8eac45d8@googlegroups.com>
Subject: A syntax for higher inductive-inductive types
MIME-Version: 1.0
Content-Type: multipart/mixed; 
	boundary="----=_Part_1381_835209206.1518089012161"

------=_Part_1381_835209206.1518089012161
Content-Type: multipart/alternative; 
	boundary="----=_Part_1382_806791265.1518089012161"

------=_Part_1382_806791265.1518089012161
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: quoted-printable

Dear all,

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

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

Andr=C3=A1s Kov=C3=A1cs
Ambrus Kaposi

------=_Part_1382_806791265.1518089012161
Content-Type: text/html; charset=utf-8
Content-Transfer-Encoding: quoted-printable

<div dir=3D"ltr">Dear all,<div><br></div><div>We have a draft titled <a hre=
f=3D"https://akaposi.github.io/hiit.pdf">&quot;A Syntax for Higher Inductiv=
e-Inductive Types&quot;</a> which may be of interest to you. There&#39;s al=
so an Agda <a href=3D"https://bitbucket.org/akaposi/elims">formalization</a=
>, and a Haskell <a href=3D"https://bitbucket.org/akaposi/elims">implementa=
tion</a> of a HIIT type/positivity checker and eliminator-generator which y=
ou can play around with. <a href=3D"https://bitbucket.org/akaposi/elims/src=
/0fd2d3e8226e08757e2ab460a5b5966e6a6fb4c4/haskell/elims-demo/examples/?at=
=3Dmaster">Here</a> are a number of examples.</div><div><br></div><div>The =
main idea is to describe HIIT-s as contexts in a &quot;domain specific&quot=
; 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 type=
s of algebras, induction methods and eliminators/beta rules by taking vario=
us models of this type theory. Non-closed HIITs and infinitary constructors=
 can be also represented by additional function spaces, with domain types b=
uilt from an &quot;external&quot; non-inductive context. We do not say anyt=
hing about existence or semantics of specified types yet.</div><div><br></d=
iv><div>Andr=C3=A1s Kov=C3=A1cs</div><div>Ambrus Kaposi</div></div>
------=_Part_1382_806791265.1518089012161--

------=_Part_1381_835209206.1518089012161--