From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.4.2 (2018-09-13) on inbox.vuxu.org X-Spam-Level: X-Spam-Status: No, score=-1.1 required=5.0 tests=DKIMWL_WL_MED,DKIM_SIGNED, DKIM_VALID,DKIM_VALID_EF,HEADER_FROM_DIFFERENT_DOMAINS, MAILING_LIST_MULTI,RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.2 Received: from mail-qk1-x73c.google.com (mail-qk1-x73c.google.com [IPv6:2607:f8b0:4864:20::73c]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 80643714 for ; Sat, 9 Feb 2019 02:01:21 +0000 (UTC) Received: by mail-qk1-x73c.google.com with SMTP id w124sf5436422qkc.14 for ; Fri, 08 Feb 2019 18:01:21 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1549677680; cv=pass; d=google.com; s=arc-20160816; b=H6tWRZjgVEHeBANr5tYdAdH4216GfIP+/UF6nqCZiIferrA8c6T27EnhOY3qjUvgm6 Jwt0MEV1hE9cm+r7nfvgWnDtUHZ4tHn1NsB2ahjguqgwDpoVhA03VPaoAeAqKLUsSuTb qXqPsQlrAJ1+qtXTB1YlUddFU2Y0RcIN4rVauVLYD9443A7zr7TA/GXCSe0wDoG8NsLu QJU2B8ffxRWznKpT8x73Jf/E6SC3nCL+oAsk0HZrGsnz0lVX+HCKdh2ZqviGxPIR8h31 gSAYXZUmbziDzKH0Zi/2SglJ8MWP8S4qgvPAer2a4aqXZqISDE2fXPM77Yfc3GuVXoKp fOkQ== ARC-Message-Signature: i=2; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=list-unsubscribe:list-archive:list-help:list-post:list-id :mailing-list:precedence:content-transfer-encoding:subject:to:from :date:references:in-reply-to:message-id:user-agent:mime-version :sender:dkim-signature; bh=mwkPT+aJo53pOD+X+i9aGCsY20bny0nkBUkeXNnQH2M=; b=BKrC3SV5EvrCP2ZeHQ6BNpRIbxVgnxeBZAF9bp/57BVIewJ3oYsk+cI5xI5IwBIlIq Nmi3mjFAQUVWy7+E2fFaIdXUU5TU7sNiN5/6PveYDuloQurjyyV9hHUTXsNOuIW4Rvft 3gS6ZCTBtCcjTa9K+9FJVpJ+MvKl53i6jL7Hb0pe5teD8NocXaLpZGUdmSYz93vyw91b YK8PHEwxXjhzi2CG7S/2rKebr5EyzNlk08GOcaeYaATBBooWFKG7d+uPfsSqKeWw9jaH LgvqP0k9UvxYjbbhpxxDMuPWLP6eWNW2A58ypAaas7ICFUsfbY0KzRpyOPxUuC1mZXDb OlUw== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@messagingengine.com header.s=fm2 header.b=E5+zp5NJ; spf=neutral (google.com: 66.111.4.26 is neither permitted nor denied by best guess record for domain of jon@jonmsterling.com) smtp.mailfrom=jon@jonmsterling.com DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:mime-version:user-agent:message-id:in-reply-to:references :date:from:to:subject:content-transfer-encoding:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=mwkPT+aJo53pOD+X+i9aGCsY20bny0nkBUkeXNnQH2M=; b=ekd3xF6AW426NpUwSp/L9Tj9LLkQBLIQ2x/hcfUkislpDAZ5TR0DLnzOTzLgsERRRu bt/okM1Z2010bE27jYTdoUWAmY11y3pSaP0HLcWXMdNeZLRHbR7QGSDSgTv35frvqArY l+LDKMMom2xphxFHt6CBHoJBXa9Z178ZWAtFF4irI/cQoz9J1uXJOu2d5pxTbh5dnoXZ oJ42iNRAuhUojAc7twlYlrCY389fjiCS8WstY9xYQQVLzXlmuOZt/3/mYvsgZ12GCMRl S/PyM8QbSbGAUryPXAkJSwfUTZssO+7zGwyG8Xa6KinprfXhjaeC9cgMiCH/Lji2sr7o hLdw== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:mime-version:user-agent:message-id :in-reply-to:references:date:from:to:subject :content-transfer-encoding:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :x-spam-checked-in-group:list-post:list-help:list-archive :list-unsubscribe; bh=mwkPT+aJo53pOD+X+i9aGCsY20bny0nkBUkeXNnQH2M=; b=FcU0eUq7LE/HlOVpkKdH7/pWfUgz5K7YPfQbKLheWcHH7hNeXuL1tkfB0gVdGhKaCF 3l/0SCvcD5XFKLCcVzxpf1VCxk5kyh1onMv/9SMuAy2WPu/89agfDJWgXgCboN7kxeB7 MUBGyIBRx/GgD4KzUmHEyBvE3e6MqTOKcUbGnaW1zrT7KsS/ll+pOsL6xic/QoGtTZUD ZTwL36qqoD7qjoI0Q+phjS6tRhvcgT6LfsLptEvP6hKmwShxA4KMCUxmBiAg0Rb7MsAF KZig4a8c5+4wUcRodqZBFAQW1l6GrouSxxk/CQ64lui5EbkOTcecUoq4gQEc8FNXAv+p ZJHg== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AHQUAubwA6HX4t0BkwTgR3Nno0K4z4nW2czxJAjdE9Jf9uby9L3/MkS1 pQH44DaIGtOmr33Q+tKYe8w= X-Google-Smtp-Source: AHgI3IbDFtH3SjONVZ0KJc0weGpNesA6qmUFwvtYEirx6DAU5fnmiIXpCln7Kii9BGe6tHbM5XIubA== X-Received: by 2002:a37:9547:: with SMTP id x68mr220007qkd.2.1549677680163; Fri, 08 Feb 2019 18:01:20 -0800 (PST) MIME-Version: 1.0 X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a0c:bc01:: with SMTP id j1ls3753750qvg.1.gmail; Fri, 08 Feb 2019 18:01:19 -0800 (PST) X-Received: by 2002:a0c:f9d0:: with SMTP id j16mr6123437qvo.15.1549677679864; Fri, 08 Feb 2019 18:01:19 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1549677679; cv=none; d=google.com; s=arc-20160816; b=vOO18vZe9pfHtbBZGDBLuZlX1RyxOK2LZKZ0FwnJ7kG0KECozPq5eOYITN6AD9Sbrn UhWu6XPJZJkfVcHbPTgb3Mf7wpC5Wb75fy0XZX4mHNO2XqGKMQXWnuwe1Shhlw6pnwRe llDUK0e2f5MmkyYlMi+DLYuQjDxP0CmEsiSRWkETmPOxaup9Ay1MpQSJOKKa4R5HrxVl I5bWp1FuHBbYcpGoNfhY292QyeVWqkFP0Bp8bflbx2mQ60T+ln//8XVB3qQJHHYyBGOr DBqVuOEqYmhqAkNDxD+ZHGos3EEgN/pUjlTkeVWIiStltretrieDu18I3ooY1yrFjeYG e68w== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=content-transfer-encoding:subject:to:from:date:references :in-reply-to:message-id:user-agent:dkim-signature; bh=pmXQbgWxSWmh4ZMgMD8xTNJiHTyY7oHr8xiVBS0AHaA=; b=Tl5qE80dCiF1OkqFgMqRKHNfxEc7XwQtYPN5zKrOemSyTjEuBcOSjMOjbIilUUD5Sq DEEXS8fJ/zRvhfnuhe0QFPAkIWkvuYzK5NbUAJe1Qv/fZBJbpLuvhNwn9tRH8XLXHFIX Sdv5QA/W44rdKeoR5d4G7qCb3lT6kvzsEdr36okBtSesjAQhD9a62hHXYUpnM0Lj5c7g 8kqDLS4nQkoqecRvkyiG1guxIsjdK0RcxFkqNNQuatjWH0dY8fl4mvE67lhH7DRQtiCO MthOiaVOnO2zPXrVJVUi1vuDaO6w3z9ljt9WEfdN54ggJuT7cy2ZpqHWOn7/Pk+D6dEf +0Ew== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@messagingengine.com header.s=fm2 header.b=E5+zp5NJ; spf=neutral (google.com: 66.111.4.26 is neither permitted nor denied by best guess record for domain of jon@jonmsterling.com) smtp.mailfrom=jon@jonmsterling.com Received: from out2-smtp.messagingengine.com (out2-smtp.messagingengine.com. [66.111.4.26]) by gmr-mx.google.com with ESMTPS id m33si171183qte.5.2019.02.08.18.01.19 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Fri, 08 Feb 2019 18:01:19 -0800 (PST) Received-SPF: neutral (google.com: 66.111.4.26 is neither permitted nor denied by best guess record for domain of jon@jonmsterling.com) client-ip=66.111.4.26; Received: from compute2.internal (compute2.nyi.internal [10.202.2.42]) by mailout.nyi.internal (Postfix) with ESMTP id 83F3F2188F for ; Fri, 8 Feb 2019 21:01:19 -0500 (EST) Received: from imap3 ([10.202.2.53]) by compute2.internal (MEProxy); Fri, 08 Feb 2019 21:01:19 -0500 X-ME-Sender: X-ME-Proxy-Cause: gggruggvucftvghtrhhoucdtuddrgedtledrleefgdefjecutefuodetggdotefrodftvf curfhrohhfihhlvgemucfhrghsthforghilhdpqfhuthenuceurghilhhouhhtmecufedt tdenucesvcftvggtihhpihgvnhhtshculddquddttddmnegoufhushhpvggtthffohhmrg hinhculdegledmnecujfgurhepofgfkfgjfhffhffvufgtgfesthhqredtreerjeenucfh rhhomhepfdflohhnucfuthgvrhhlihhnghdfuceojhhonhesjhhonhhmshhtvghrlhhinh hgrdgtohhmqeenucffohhmrghinhepghhoohhglhgvrdgtohhmnecurfgrrhgrmhepmhgr ihhlfhhrohhmpehjohhnsehjohhnmhhsthgvrhhlihhnghdrtghomhenucevlhhushhtvg hrufhiiigvpedt X-ME-Proxy: Received: by mailuser.nyi.internal (Postfix, from userid 501) id 21B857C1E5; Fri, 8 Feb 2019 21:01:19 -0500 (EST) X-Mailer: MessagingEngine.com Webmail Interface User-Agent: Cyrus-JMAP/3.1.5-832-gba113d7-fmstable-20190201v1 X-Me-Personality: 19972253 Message-Id: <431cad6d-062a-4ed8-8c01-c6caf884ffa8@www.fastmail.com> In-Reply-To: References: <1a3dfba4-816a-42c3-8eea-1a2906cb1cad@googlegroups.com> Date: Fri, 08 Feb 2019 20:58:28 -0500 From: "Jon Sterling" To: "'Martin Escardo' via Homotopy Type Theory" Subject: Re: [HoTT] Re: Why do we need judgmental equality? Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable X-Original-Sender: jon@jonmsterling.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@messagingengine.com header.s=fm2 header.b=E5+zp5NJ; spf=neutral (google.com: 66.111.4.26 is neither permitted nor denied by best guess record for domain of jon@jonmsterling.com) smtp.mailfrom=jon@jonmsterling.com Precedence: list Mailing-list: list HomotopyTypeTheory@googlegroups.com; contact HomotopyTypeTheory+owners@googlegroups.com List-ID: X-Google-Group-Id: 1041266174716 List-Post: , List-Help: , List-Archive: , Hi Valery, I'm trying to square what you said with what Anders said. Consider extendin= g MLTT with an interval in two different ways: 1. With judgmental computation rules for the recursor 2. With propositional computation axioms for the recursor I do not expect to obtain a conservativity result for the second version ov= er the first version, since the first one derives function extensionality, = and the second one does not (afaict). Can you give a bit more detail about how this algebraic power move that you= are describing works, and whether it applies in this case? Thanks! Jon On Fri, Feb 8, 2019, at 6:32 PM, Valery Isaev wrote: > If you are not interested in computations and convenience of your type=20 > theory, then the definitional equality is not essential in the sense=20 > that every type theory T is equivalent to a type theory Q(T) with no=20 > computational rules. Now, what do I mean when I say that type theories=20 > T and Q(T) are equivalent? I won't give here the formal definition, but= =20 > the idea is that Q(T) can be interpreted in T and, for every type A of=20 > T, there is a type in Q(T) equivalent to A in T and the same is true=20 > for terms. This implies that every statement (i.e., type) of Q(T) is=20 > provable in Q(T) if and only if it is provable in T and every statement= =20 > of T has an equivalent statement in Q(T), so the theories are=20 > "logically equivalent". Moreover, equivalent theories have equivalent=20 > (in an appropriate homotopical sense) categories of models. >=20 > Regards, > Valery Isaev >=20 >=20 > =D1=81=D0=B1, 9 =D1=84=D0=B5=D0=B2=D1=80. 2019 =D0=B3. =D0=B2 00:19, Mart= =C3=ADn H=C3=B6tzel Escard=C3=B3 : > > I would also like to know an answer to this question. It is true that d= ependent type theories have been designed using definitional equality. > >=20 > > But why would anybody say that there is a *need* for that? Is it imposs= ible to define a sensible dependent type theory (say for the purpose of ser= ving as a foundation for univalent mathematics) that doesn't mention anythi= ng like definitional equality? If not, why not? And notice that I am not ta= lking about *usability* of a proof assistant such as the *existing* ones (s= ay Coq, Agda, Lean) were definitional equalities to be removed. I don't car= e if such hypothetical proof assistants would be impossibly difficult to us= e for a dependent type theory lacking definitional equalities (if such a th= ing exists). > >=20 > > The question asked by Felix is a very sensible one: why is it claimed t= hat definitional equalities are essential to dependent type theories? > >=20 > > (I do understand that they are used to compute, and so if you are inter= ested in constructive mathematics (like I am) then they are useful. But, ag= ain, in principle we can think of a dependent type theory with no definitio= nal equalities and instead an existence property like e.g. in Lambek and Sc= ott's "introduction to higher-order categorical logic". And like was discus= sed in a relatively recent message by Thierry Coquand in this list,) > >=20 > > Martin=20 > >=20 > >=20 > > On Wednesday, 30 January 2019 11:54:07 UTC, Felix Rech wrote: > >> In section 1.1 of the HoTT book it says "In type theory there is also = a need for an equality judgment." Currently it seems to me like one could, = in principle, replace substitution along judgmental equality with explicit = transports if one added a few sensible rules to the type theory. Is there a= fundamental reason why the equality judgment is still necessary? > >>=20 > >> Thanks, > >> Felix Rech > > =20 >=20 >=20 > > --=20 > > 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/optout. > > =20 > =20 >=20 >=20 > --=20 > You received this message because you are subscribed to the Google=20 > Groups "Homotopy Type Theory" group. > To unsubscribe from this group and stop receiving emails from it, send= =20 > an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. > For more options, visit https://groups.google.com/d/optout. > --=20 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 e= mail to HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout.