From mboxrd@z Thu Jan  1 00:00:00 1970
Date: Wed, 13 Sep 2017 02:42:49 -0700 (PDT)
From: Paolo Capriotti <p.cap...@gmail.com>
To: Homotopy Type Theory <HomotopyT...@googlegroups.com>
Message-Id: <9b7e0489-0762-49cf-92f3-512652fd3ae5@googlegroups.com>
In-Reply-To: <53258baf-7832-4919-8ab1-3e653c97241a@googlegroups.com>
References: <53258baf-7832-4919-8ab1-3e653c97241a@googlegroups.com>
Subject: Re: Characterizing the equality of Indexed W types
MIME-Version: 1.0
Content-Type: multipart/mixed; 
	boundary="----=_Part_3998_1395408500.1505295769410"

------=_Part_3998_1395408500.1505295769410
Content-Type: multipart/alternative; 
	boundary="----=_Part_3999_354255266.1505295769410"

------=_Part_3999_354255266.1505295769410
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 7bit

On Wed, Sep 13, 2017, at 05:41 AM, Jasper Hugunin wrote:
> I am not aware of these results in any of the literature; hopefully they 
> are a useful contribution to the understanding of inductive types in ITT

I have a similar development here: 
https://github.com/pcapriotti/agda-base/tree/master/.  Look in 
`src/container/w`.

BR,
Paolo

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

<div dir=3D"ltr"><div>On Wed, Sep 13, 2017, at 05:41 AM, Jasper Hugunin=C2=
=A0wrote:</div><div>&gt; I am not aware of these results in any of the lite=
rature; hopefully they=C2=A0</div><div>&gt; are a useful contribution to th=
e understanding of inductive types in ITT</div><div><br></div><div>I have a=
 similar development here: https://github.com/pcapriotti/agda-base/tree/mas=
ter/. =C2=A0Look in `src/container/w`.</div><div><br></div><div>BR,</div><d=
iv>Paolo</div></div>
------=_Part_3999_354255266.1505295769410--

------=_Part_3998_1395408500.1505295769410--