From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.107.104.8 with SMTP id d8mr25905403ioc.79.1509357176315; Mon, 30 Oct 2017 02:52:56 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.36.111.14 with SMTP id x14ls1939983itb.2.canary-gmail; Mon, 30 Oct 2017 02:52:55 -0700 (PDT) X-Received: by 10.107.222.8 with SMTP id v8mr25522538iog.12.1509357175555; Mon, 30 Oct 2017 02:52:55 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1509357175; cv=none; d=google.com; s=arc-20160816; b=naEsJZSBO0aY6FFHTstPSXX8CuRD+qmexqYQDhUH5rDw3Otlivd9cygEQYOBFpuIsa kbrXRSpD+vXlX/vmC2b7iczsCat4EA8msPLNx9/CFW8HWTlukMwLG4TdSQQS7WfNchFL PjxYNz9ajdm6wK/50V0zZbcJDeqzvqIe2gWZdMDgp+U8ICb0J9MTkbc9RWbthOnJyCS6 B76QVREOoB6H8l2VHCV4udsZ+MJUTBrPAn0IvsbcSL7ZG/tNtvoJsuqBM88y+fDe3XdF hh1SIKMpUYqcsGQNGQTxER9RIveBPTvHCKp7FR+z4W5Et/euTv1QihMu8FKrG/DqHJPD sXxw== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=content-transfer-encoding:cc:to:subject:message-id:date:from :references:in-reply-to:mime-version:dkim-signature :arc-authentication-results; bh=HyUtxVcC45xNb/k1UULzUpJx4N5XHSr5H8pyPWaqK6Q=; b=g5tvh66jBTvYr5VVsk6Pr5jRAVapTIHiO/qGfWRlMN9WpPyB+Ifg65yFbLRjGaAOt9 PUi7a27sx3h43RuExeKp7vHuUZpaBE+32/C1U0D7kddvNGFBFmUmbrbi0vIVgFyRM/LF 1yi++/mGZCxnts/ST5PJJYiRY2RifqFeB3KpZ/Zlsn6jJcj8bjx2rx7iPyU8tPl8OYfB 4im7snZVLkYaT+fWUzz6UGTgkPj4Hn9TQISJBMzDGDnaMin+xW/uPFX1lP9JuQkEnjkO ZUwqjStVCoUxbXyxoR/24T2eSCsKkBSwdNiE0OJBASqHgvETAj6M6g1ySnJvPAsQtPhE wB/A== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=DcLtFvjF; spf=pass (google.com: domain of sanz...@gmail.com designates 2607:f8b0:4001:c06::22d as permitted sender) smtp.mailfrom=sanz...@gmail.com; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=gmail.com Return-Path: Received: from mail-io0-x22d.google.com (mail-io0-x22d.google.com. [2607:f8b0:4001:c06::22d]) by gmr-mx.google.com with ESMTPS id o133si157000itc.1.2017.10.30.02.52.55 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Mon, 30 Oct 2017 02:52:55 -0700 (PDT) Received-SPF: pass (google.com: domain of sanz...@gmail.com designates 2607:f8b0:4001:c06::22d as permitted sender) client-ip=2607:f8b0:4001:c06::22d; Authentication-Results: gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=DcLtFvjF; spf=pass (google.com: domain of sanz...@gmail.com designates 2607:f8b0:4001:c06::22d as permitted sender) smtp.mailfrom=sanz...@gmail.com; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=gmail.com Received: by mail-io0-x22d.google.com with SMTP id i38so25768209iod.2 for ; Mon, 30 Oct 2017 02:52:55 -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:content-transfer-encoding; bh=HyUtxVcC45xNb/k1UULzUpJx4N5XHSr5H8pyPWaqK6Q=; b=DcLtFvjFAOQG3xq+ht1yiODHPJu+5tXBxBzachRd8DbeFMW0u3PhHkC9rXPmxVspvl q/nHVl9yZbtfdIor5KxW1k0ByFm1WRMt+g1bKFXHZuvCmhu7Pp2sIYrte5JpuVm3DLuY y7Ur0E3MSL+H+iPC2tDHnTgdGdSujbGOW1yet7u+LKBLME/2Fvdk9pY8l7kFSZd2vFcc 3TLUn47x6Ea1rWdYmsd+1eH2PgLJVcQrB6uFAVdEzbUKxibz3g+ZxcLSqo63p1uB8Fnd hfQdEUUhC+7j01E+/kRRPz6yX6yJH954dx7eWcLlebvSA0xcWXzYPSFXGeLoav/zXy00 GkDw== X-Gm-Message-State: AMCzsaUGWiOQ8ewt1ZTPwgB6JqUNDBR3FrDnOvYUcy0iYNDHeEekzQGW NUpGfEBvOVZKTFoVPcvsgL+FJzF0pgJvVndTs2khpA== X-Received: by 10.36.55.210 with SMTP id r201mr5069390itr.132.1509357175161; Mon, 30 Oct 2017 02:52:55 -0700 (PDT) MIME-Version: 1.0 Received: by 10.107.200.79 with HTTP; Mon, 30 Oct 2017 02:52:54 -0700 (PDT) In-Reply-To: References: <242584a5-d5fa-fcfe-a29e-61e51d4575fe@gmail.com> From: Andrea Vezzosi Date: Mon, 30 Oct 2017 10:52:54 +0100 Message-ID: Subject: Re: [HoTT] Re: Canonical forms for initiality To: Michael Shulman Cc: Neel Krishnaswami , Homotopy Type Theory Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable To maybe add a third way: you can define the graph of hereditary substition as a proposition if you have already proven judgmental equality is decidable. Let me write "=CE=93 =E2=8A=A2 e : A" for the typing judgment where =CE=93,= e, and A are not necessarily in normal form, and "(e , d) [[ =CF=83 ]]" for type-preserving non-hereditary substitution for a typing derivation d. Defining hereditary substitution mutually with the syntax seems like a huge task to me because it involves a proof that your language is normalizing, and I wouldn't want to convince any I-R schema that the whole construction is well-founded. However if one first proves that judg. equality is decidable for "=CE=93 = =E2=8A=A2 e : A"[1], then we can define t1 [ =CF=83 ] =3D t2 :=3D isTrue (decideEq ((U-term t1) [[ U-subst =CF=83 ]= ]) (U-term t2)) where U is a function defined by I-R which converts normal form judgments back into expressions and typing judgments; for both terms, types, contexts and substitutions: U-term : =CE=93 =E2=8A=A2 A =E2=86=92 =CE=A3 (e : Expr). fst (U-cxt =CE=93)= =E2=8A=A2 e : fst (U-type A) After the fact It should then be possible to show that the normal form judgments are a set, and then define an actual substitution function. However I don't know if this construction would still satisfy what we want out of a type of normal forms? Would that be an initiality theorem for a class of models? What class? Best, Andrea [1] Like here https://github.com/mr-ohman/logrel-mltt , but I'd expect a proof with intrinsic typing like https://arxiv.org/abs/1612.02462 to also work. [1] https://github.com/mr-ohman/logrel-mltt On Fri, Oct 20, 2017 at 1:16 PM, Michael Shulman wrot= e: > Good question! I can think of three reasons: > > 1. We still don't know whether inductive-recursive definitions make > sense homotopically. > 2. In my limited experience, inductive-inductive definitions generally > have more powerful induction principles than inductive-recursive ones. > In particular, it's much less clear to me that with an > inductive-recursive definition we could map out of it into any > (oo,1)-category. > 3. I'm less confident than you that the inductive-recursive case would > be easier. My experience with this sort of thing leads me to believe > that it's like playing whack-a-mole: if you think you solve the > coherence problem in one way then it pops up somewhere else. But > someone should try it! > > Mike > > On Fri, Oct 20, 2017 at 3:57 AM, Neel Krishnaswami > wrote: >> Hi Mike, >> >> Why do you prefer this style of definition to specifying the hereditary >> substitution as a function (using an inductive-recursive definition)? It >> seems like that would give you all the coherences you want since all >> the substitution equations would hold judgmentally.[*] >> >> I do want to see it worked out your way, now that you've told me about >> it, but that's because doing the same thing two ways is usually >> clarifying. However, the "obvious" way to generalize the simply-typed >> presentation is with an inductive-recursive definition. >> >> Best, >> Neel >> >> [*] I think?, since I haven't done the proofs. >> >> On 19/10/17 20:07, Michael Shulman wrote: >>> >>> On Tue, Oct 17, 2017 at 9:00 AM, Matt Oliveri wrote: >>>> >>>> Could you explain why you want to use normal forms and hereditary >>>> substitution--rather than more typical typing rules--if you expect to >>>> need >>>> an infinite tower of coherences anyway? Needing the coherence tower se= ems >>>> like it will make the definition dramatically more complicated, so >>>> wouldn't >>>> it be best to base it on the most simple and familiar typing rules? >>> >>> >>> The advantage of canonical forms and hereditary substitution is that >>> the object-language judgmental equality automatically coincides with >>> the metatheoretic equality, and the inductive-inductive syntax should >>> simultaneously automatically form a set. If we instead build a >>> coherence tower of judgmental equalities and higher judgmental >>> equalities, then we not only need to decide what that coherence >>> structure should be (whereas I think the coherence structure for >>> hereditary substitution should be fairly straightforward in >>> principle), but prove that it is "coherent" in some sense, in order to >>> enable the interpretation of raw syntax into inductive-inductive >>> syntax. >> >> >> >> >> -- >> You received this message because you are subscribed to the Google Group= s >> "Homotopy Type Theory" group. >> To unsubscribe from this group and stop receiving emails from it, send a= n >> email to HomotopyTypeThe...@googlegroups.com. >> For more options, visit https://groups.google.com/d/optout. > > -- > 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.