From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.129.52.79 with SMTP id b76mr11394170ywa.209.1505303271010; Wed, 13 Sep 2017 04:47:51 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.107.6.170 with SMTP id f42ls2856402ioi.12.gmail; Wed, 13 Sep 2017 04:47:50 -0700 (PDT) X-Received: by 10.55.209.202 with SMTP id o71mr9459016qkl.2.1505303270219; Wed, 13 Sep 2017 04:47:50 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1505303270; cv=none; d=google.com; s=arc-20160816; b=JPs+nMe8KgFFU9izZS2B0EsUX+Rf0xtdcbsj4SwRXEE7AKChOATa3S3/3O598qM3ph UW0l1ESYCmXgLl1suDFa6pH7yD5lvFEcd1YnL3wIuTp0MbyMg+45ErSouVTpwFFOioa6 J05hhKBoWTVFAz8xjpUkTa54ST8bnPPWjRE3jY9k3s6CM2jejcATer56uD6qKnJShD8k hYkAPcDsDyvwnnzOlzVBDB5LsdbqMSB6cMvtNvz/z2UfcrfVzFUOFOY0LnNECOq/RBSw QGAp//QfexGdermmlNh7khFPDFgsQ1kqbGmowJrTc4p3Ey3XpelxK9b/0tpCBui4Xquw 0xjQ== 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=a2Oe+IkSZ+ju9/3P/7RlxrOrJibVI8euJLwG3cl0FcE=; b=vP2p45RMVXrP1fNI039CVqdjtW0csfAKME0kD/43wSVV8qIHG0Go171v+ygRVDHO2b kUMA2oByWntVX1eGG0wzYdOMEDPQSHj4oPXnfQ5GlDpbpRk55o+PWCjNbzouDaYNO0P7 JG7ZsGUFkgER9I8dW8coCN8Bkzq7LfUKHKqH3iDgAsjHaXUCINgqGXgfGKvbiFusddRx cWDruWZCOukwTIIVb0cKVoE3B+YeDSMY/Z/kEl2WoJFOteABmp6w02JRFUf9CIDgy0z9 YfStit9tAr/0xUj7oFipVyyPsMjTBA4XnhrLdToO9wPjgg6TjyIr9da0ZP004NASRB/M a0Zg== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=lG2Vzaqe; spf=pass (google.com: domain of b.a.w.s...@gmail.com designates 2607:f8b0:400c:c05::232 as permitted sender) smtp.mailfrom=b.a.w.s...@gmail.com; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=gmail.com Return-Path: Received: from mail-vk0-x232.google.com (mail-vk0-x232.google.com. [2607:f8b0:400c:c05::232]) by gmr-mx.google.com with ESMTPS id n19si750344vkf.13.2017.09.13.04.47.50 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Wed, 13 Sep 2017 04:47:50 -0700 (PDT) Received-SPF: pass (google.com: domain of b.a.w.s...@gmail.com designates 2607:f8b0:400c:c05::232 as permitted sender) client-ip=2607:f8b0:400c:c05::232; Authentication-Results: gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=lG2Vzaqe; spf=pass (google.com: domain of b.a.w.s...@gmail.com designates 2607:f8b0:400c:c05::232 as permitted sender) smtp.mailfrom=b.a.w.s...@gmail.com; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=gmail.com Received: by mail-vk0-x232.google.com with SMTP id w23so6991433vkw.2 for ; Wed, 13 Sep 2017 04:47:50 -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=a2Oe+IkSZ+ju9/3P/7RlxrOrJibVI8euJLwG3cl0FcE=; b=lG2VzaqeHxB8Wny8xA4zJo1kWEaXgpsT1V1HGgnYjcZ/mhb017iQVndNeChnMcJUL0 +eloW9j/5QKbKpH5pROwnniStZXjdWD7UiYCa6lJ89CDnq5yekHvoIBz/5DKgRvFDlnL 6a9H7kVikXPOh2O6alFfR7wjJjCgrL7SmMUWLTUtFZQD3VIPLaYOIW5sgsmFj5yFrvEv lUSpWbOdMdaKdeOcszcHMTIBGfnEiDn4PrDqC7HwsBeZ7nj5xJdm9Z/D9yRBy8RCI5uj KhUWLudKpJVoxLnuPCCwrqiUy9W/qMucRGW44CdijYeCM3guCnt/CDSPWs0DGi8HQjU4 Eo7A== X-Gm-Message-State: AHPjjUjE7t3NalraBu3QHSRkTUxQxeiTJGJuKdS1IZ3uu9bETzv+bc6H MiNXESdugGfhUkGakRMdCQW7NUNuYl07I30Gov0= X-Received: by 10.31.63.12 with SMTP id m12mr12453530vka.26.1505303269905; Wed, 13 Sep 2017 04:47:49 -0700 (PDT) MIME-Version: 1.0 Received: by 10.103.124.68 with HTTP; Wed, 13 Sep 2017 04:47:29 -0700 (PDT) In-Reply-To: References: <53258baf-7832-4919-8ab1-3e653c97241a@googlegroups.com> From: Bas Spitters Date: Wed, 13 Sep 2017 12:47:29 +0100 Message-ID: Subject: Re: [HoTT] Characterizing the equality of Indexed W types To: Christian Sattler , Peter LeFanu Lumsdaine Cc: jas...@cs.washington.edu, Thorsten Altenkirch , Homotopy Type Theory Content-Type: text/plain; charset="UTF-8" Thanks. I have updated the nlab and also included links to the three formalizations. https://ncatlab.org/nlab/show/inductive+family @Peter, if your formalization is available, we should add a link too. On Wed, Sep 13, 2017 at 12:05 PM, Christian Sattler wrote: > 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_categorical_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. > >