From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.176.78.238 with SMTP id x46mr11864842uah.54.1505300707964; Wed, 13 Sep 2017 04:05:07 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.36.127.21 with SMTP id r21ls2967113itc.11.canary-gmail; Wed, 13 Sep 2017 04:05:07 -0700 (PDT) X-Received: by 10.36.4.20 with SMTP id 20mr1598341itb.13.1505300707120; Wed, 13 Sep 2017 04:05:07 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1505300707; cv=none; d=google.com; s=arc-20160816; b=aqCTcW2cwDx7FwmEjm5nXiVRjso8Dup7OStdITmT/SdAmEFz9SqEuKHwbcyo/HhmUk 6b01uIx6+r+eWf4cjPEn11FUCO3eouwwI6C+AOOgapjnfiXIJwKN8sldOeZQgzyf4W8n OnJVXm6wB1Ea81yVpyUq5NK6ag7XPuUi1DMtzlUZrtKP3ZwRT43W7vZaJsUt/oVgM9hV 7tZZl54Pb9Yglyalr+PAU/HrAp17EsgOjoIjpeZyfTq+AaAJQPHtq6LjWTT0vSO1NFuu oR+glXfYCVEMHv5MeC7lCOufbrn4BNDl7mNteDqmfkyVOL45UbmBGcx7KdLu8Wx47lqN nlOg== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=cc:to:subject:message-id:date:from:references:in-reply-to :mime-version:dkim-signature:arc-authentication-results; bh=5J171h+s6Pb/LmZpvvCMkW+L4foU+2iPeQaeST+GqK0=; b=J6Y41qIDAWdx/nXsw5MyR3AgvRxQ0LT6v7khXl0ll3bHV/zzhWpwjAw+ndBQFbk80W 8s5vM693JHqjbFd184otdfkqucqHz8UNFSvl9DTVGPInjJEb3O2eEytwIE0Yn7kR5ciA NtRzNOfBZ5dABaer1xhChvl9/w7faa5QLrUSAA22eSmLhv35hvV88LX2BNCmOb5Ha7XE ZtbXtrWXeJkmVE7hVPcyJwNBhg8reNhCTPwex7SOsVn+wW++ZzYV3u7sntFXjqutupGV w+MNqAfQ/t0R2id8hJ94sYjMi0e24AQPmPlxxwLmMt7GJATVa9Fri/+1wUbDA8qJFVN6 N/yg== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=e/LEXG5j; spf=pass (google.com: domain of sattler....@gmail.com designates 2607:f8b0:400e:c00::230 as permitted sender) smtp.mailfrom=sattler....@gmail.com; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=gmail.com Return-Path: Received: from mail-pf0-x230.google.com (mail-pf0-x230.google.com. [2607:f8b0:400e:c00::230]) by gmr-mx.google.com with ESMTPS id a17si1394149pfk.15.2017.09.13.04.05.07 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Wed, 13 Sep 2017 04:05:07 -0700 (PDT) Received-SPF: pass (google.com: domain of sattler....@gmail.com designates 2607:f8b0:400e:c00::230 as permitted sender) client-ip=2607:f8b0:400e:c00::230; Authentication-Results: gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=e/LEXG5j; spf=pass (google.com: domain of sattler....@gmail.com designates 2607:f8b0:400e:c00::230 as permitted sender) smtp.mailfrom=sattler....@gmail.com; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=gmail.com Received: by mail-pf0-x230.google.com with SMTP id e1so22929999pfk.1 for ; Wed, 13 Sep 2017 04:05:07 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc; bh=5J171h+s6Pb/LmZpvvCMkW+L4foU+2iPeQaeST+GqK0=; b=e/LEXG5j9jp3lGHfe/BkefiNoE1Mp5BFgU06TEzvHO1Tvr2snwtQ/LUaJQ5eEPmHZH V3Wtj9kvnk07Qs6DO6Drm3WS7VUUGdywJTkehYKvWfL24t/TLx6sQaFoS2g6aqyP5LKy a2uxgjw8PyCYjki+48DyOJoa8iYjnhoWTDDy+P7KZdmCWs2ksRFYlsklFfSt3g46cAho UfdZgPzXDQPVV1x0IDK4d6aNToF0JZ1da7yt7oXHoixXP7at29uGsFp6UAYsFHKqB5ac hgjhA6nWwyRUlA9/G+42zbG/yk0hX6XiOuSK6Dg8gJr1zTdhsgJk/+5vZhW+ZqFMwr+M Ubfg== X-Gm-Message-State: AHPjjUiww2XXqpzX+/f31Rzayh/f07U/A4lMC4Zrx68ok2vLWbe1GDSV e45rv364aRWybjHyIlZ07uNhzQQEaJY1PJzB4jk= X-Received: by 10.99.7.205 with SMTP id 196mr17378655pgh.356.1505300706838; Wed, 13 Sep 2017 04:05:06 -0700 (PDT) MIME-Version: 1.0 Received: by 10.100.183.110 with HTTP; Wed, 13 Sep 2017 04:05:06 -0700 (PDT) In-Reply-To: References: <53258baf-7832-4919-8ab1-3e653c97241a@googlegroups.com> From: Christian Sattler Date: Wed, 13 Sep 2017 13:05:06 +0200 Message-ID: Subject: Re: [HoTT] Characterizing the equality of Indexed W types To: Bas Spitters Cc: jas...@cs.washington.edu, Thorsten Altenkirch , Homotopy Type Theory Content-Type: multipart/alternative; boundary="94eb2c085842e94b1a05591021bf" --94eb2c085842e94b1a05591021bf Content-Type: text/plain; charset="UTF-8" On Wed, Sep 13, 2017 at 9:50 AM, Bas Spitters wrote: > Dear Jasper, > > Thanks. This is a nice result. > > Thorsten and Christian will correct me, but I believe the reduction > from indexed W-types to W-types was not fully worked out in HoTT > before. > All reductions (be it in extensional TT or MLTT with funext) that I know of carve the (homotopy) indexed W-type X out of a "larger" (homotopy) W-type Y. In book-style HoTT (where one has enough nice universes), the carving out can be done simply by defining a "predicate" P : Y -> U (not valued in propositions in general) by recursion on Y and letting X = (y : Y) x P(y). I believe I've seen Coq code by Peter Lumsdaine from quite a while ago doing this. But even without large elimination, the carving out can still be done using a certain coreflexive equalizer, just like Gambino-Hyland do it for extensional type theory using a equalizer (also coreflexive, but which doesn't matter in the 1-categorical context). I wanted to write this up nicely for a quite a while now, but I am still lacking a nice way of talking about internal higher functors and so on without universes. Christian > > Christian announced a beautiful route to it using ideas from higher > category theory, but I don't think the full details in HoTT ever > appeared. > I've tried to collect references here: > https://ncatlab.org/nlab/show/inductive+family#higher_catego > rical_version_homotopy_type_theory > > I think it would be nice to add your results both to the HoTT library > and to Unimath. > > Best regards, > > Bas > > On Wed, Sep 13, 2017 at 5:41 AM, wrote: > > Hello, > > > > I have uploaded to GitHub a Coq development characterizing the equality > of > > Indexed W types (dependent W types, inductive families) up to > equivalence, > > as an Indexed W type. > > > > https://github.com/jashug/IWTypes > > > > We define an Indexed W type as an inductive family, where every node in a > > regular W type is assigned an index. > > We then show that the types a = b are inductively generated by (sup x > > children1) = (sup x children2) with children (children1 c = children2 c). > > > > Calling the map from the data of a node to its index f, we show if the > > fibers of f have positive h-level, then the Indexed W type has the same > > h-level. > > Assuming the children are finite enumerable, we also show that decidable > > equality is inherited from the fibers of f. > > > > 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 / > HoTT. > > Please send any comments, questions or suggestions. > > > > - Jasper Hugunin > > > > -- > > You received this message because you are subscribed to the Google Groups > > "Homotopy Type Theory" group. > > To unsubscribe from this group and stop receiving emails from it, send an > > email to HomotopyTypeThe...@googlegroups.com. > > For more options, visit https://groups.google.com/d/optout. > --94eb2c085842e94b1a05591021bf Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
On W= ed, Sep 13, 2017 at 9:50 AM, Bas Spitters <b.a.w.s...@gmail.com>= wrote:
Dear Jasper,

Thanks. This is a nice result.

Thorsten and Christian will correct me, but I believe the reduction
from indexed W-types to W-types was not fully worked out in HoTT
before.

All reductions (be it in extens= ional TT or MLTT with funext) that I know of carve the (homotopy) indexed W= -type X out of a "larger" (homotopy) W-type Y.

In book-style HoTT (where one has enough nice universes), the carvin= g out can be done simply by defining a "predicate" P : Y -> U = (not valued in propositions in general) by recursion on Y and letting X =3D= (y : Y) x P(y). I believe I've seen Coq code by Peter Lumsdaine from q= uite a while ago doing this.

But even without larg= e elimination, the carving out can still be done using a certain coreflexiv= e equalizer, just like Gambino-Hyland do it for extensional type theory usi= ng a equalizer (also coreflexive, but which doesn't matter in the 1-cat= egorical context). I wanted to write this up nicely for a quite a while now= , but I am still lacking a nice way of talking about internal higher functo= rs and so on without universes.

Christian
=C2=A0

Christian announced a beautiful route to it using ideas from higher
category theory, but I don't think the full details in HoTT ever
appeared.
I've tried to collect references here:
https:= //ncatlab.org/nlab/show/inductive+family#higher_categorical_versi= on_homotopy_type_theory

I think it would be nice to add your results both to the HoTT library
and to Unimath.

Best regards,

Bas

On Wed, Sep 13, 2017 at 5:41 AM,=C2=A0 <jas...@cs.washington.edu> wrote:
> Hello,
>
> I have uploaded to GitHub a Coq development characterizing the equalit= y of
> Indexed W types (dependent W types, inductive families) up to equivale= nce,
> as an Indexed W type.
>
> https://github.com/jashug/IWTypes
>
> We define an Indexed W type as an inductive family, where every node i= n a
> regular W type is assigned an index.
> We then show that the types a =3D b are inductively generated by (sup = x
> children1) =3D (sup x children2) with children (children1 c =3D childr= en2 c).
>
> Calling the map from the data of a node to its index f, we show if the=
> fibers of f have positive h-level, then the Indexed W type has the sam= e
> h-level.
> Assuming the children are finite enumerable, we also show that decidab= le
> equality is inherited from the fibers of f.
>
> I am not aware of these results in any of the literature; hopefully th= ey are
> a useful contribution to the understanding of inductive types in ITT /= HoTT.
> Please send any comments, questions or suggestions.
>
> - Jasper Hugunin
>
> --
> You received this message because you are subscribed to the Google Gro= ups
> "Homotopy Type Theory" group.
> To unsubscribe from this group and stop receiving emails from it, send= an
> email to HomotopyTypeTheory+unsubscribe@googlegroups.com.
> For more options, visit https://groups.google.com/d/opto= ut.

--94eb2c085842e94b1a05591021bf--