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=DKIM_SIGNED,DKIM_VALID, DKIM_VALID_AU,DKIM_VALID_EF,FREEMAIL_FORGED_FROMDOMAIN,FREEMAIL_FROM, HEADER_FROM_DIFFERENT_DOMAINS,HTML_MESSAGE,MAILING_LIST_MULTI, RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.2 Received: from mail-pg1-x540.google.com (mail-pg1-x540.google.com [IPv6:2607:f8b0:4864:20::540]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id df2fe44a for ; Sat, 9 Feb 2019 08:05:08 +0000 (UTC) Received: by mail-pg1-x540.google.com with SMTP id e34sf4183981pgm.1 for ; Sat, 09 Feb 2019 00:05:07 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1549699506; cv=pass; d=google.com; s=arc-20160816; b=HOT91222XT2P3Gaee/d/ktlHS/lz30+tzaRyRjxXxr4Rf8NqCxc+VhiWnVHn2EolrT EF3T6amG3vJKd7zsXn2inMeNmxMFHUPktTnErZGXM5uj1p5NgJLafv7QrNcIbSTSoQhx 38yzA7o6lB7Ja8DBDbr2z0tn+iKuFdOYMzHq6aZFglLQ2Tih4HNy+i3M/UcN7P8M8iyy bcUgqBKBI+LcPoMO/EgfxArSUGiy0uuaBSs2O9sNrvdXLj2aRbwnhL38lJstmAo60lzd UXvKGJBk/ETEGaCQ23NSe5h6kR5+5oUk0ng+XlCkR2XAjVjb6iXuoxv0cmzEHV1u5JJZ CLdw== 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:cc:to:subject:message-id:date:from :in-reply-to:references:mime-version:sender:dkim-signature :dkim-signature; bh=n+O4DPg+V9R28HxcG8TJ/EEG04uTD4ZDcN7fLKlGor4=; b=C1D+JPvQIQf0whlUFO4761K5hr8/lCeFAJnlFvGTCk1tYbwpLahpZVHJZmeqeyomSx xuyOy6Dt62v2We88WmjSXfsxpU56PkRroV3ahUKZa35zHnSMGE6TRhdUbVj1D6GfUYQ8 52/sFR4HMbwSa8LzM+4GM1jU4ucBAvRbIAl0lrrMJG4lNyIf8tVyQ4xFZp1u5WeUPEjT AgW+grTDbGMDRkXz5PsdeuYzZuyphSJ8s8maJE968naPmAPHpy+kHFztjjYrDOTAK6RH zkByXhoAAHyRiaC2Lok7JM+EXAcaShWa1TAmEa/X/sLpGkawbmYrmKYo4yFQdJvfErt3 yrsw== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b="UwPK/DIj"; spf=pass (google.com: domain of valery.isaev@gmail.com designates 2607:f8b0:4864:20::12a as permitted sender) smtp.mailfrom=valery.isaev@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:mime-version:references:in-reply-to:from:date:message-id :subject:to:cc:x-original-sender:x-original-authentication-results :precedence:mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=n+O4DPg+V9R28HxcG8TJ/EEG04uTD4ZDcN7fLKlGor4=; b=fP7MHGBn/AiPUcm821LTMw9GZwxmIQDtA8F6ObHSbGsxADJqSAsh4r21z6uISGFpUB GF89CcQt++NFF0gPtJF3XAzrmxdB+GuM5ZA7NLw6OCmnHl9GmOcxX7UP7zSyldbMoaan 77BpY4uUm/jV0S3hWqX4vP01Ill0Ab832RSYcogeTLccTc5m+dPdIjp0R4ORqQAEDeAk tZiLmrm7RAahudwTr/rExi+FL9Ky68kudUSLstJyqCbm9dVPzcaYzZ9g4JvmQyO1Wf6I +DLqiojIpi6XJa8qrMqbx60AoCt4+mXuoOdDqAWYQxMQIqbN1CP/CZ1tP6yfPxxW1YsT MwVg== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version:references:in-reply-to:from:date:message-id:subject:to :cc:x-original-sender:x-original-authentication-results:precedence :mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=n+O4DPg+V9R28HxcG8TJ/EEG04uTD4ZDcN7fLKlGor4=; b=FHgBvS+QwqUiiBI/71bi8QYUbuti+YjcQzDp2NbzjKebJSecV4sp8TK63bOkRj2JPH vdDfsCbFrKIrIgesj7E81Jz3tYyboJcY2pEcNF8DEltE9mG8TeFNWzX8d7THCo4r1wXW U76CFKnAfaFSet3U3KlTZAawWcNGBDXDWzfv1e5vvfdYeTK5ZUEyEsXD18QHQvvXkx+z NdffmV0hx3yVmbIBBjR9Mrj4JFJ3n5QRJ2/e5hrIT7rx/JKAItPnQKUkKSu04nEfYtja x4ZRXnR3NMdDUbNI9pmPzM7RAXyDFQBQ0CFLT2u1B6PIZT1LNuBlbcHrIJoFreDl4ZG3 pvRQ== 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:references:in-reply-to:from :date:message-id:subject:to:cc: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=n+O4DPg+V9R28HxcG8TJ/EEG04uTD4ZDcN7fLKlGor4=; b=Zu82PC8VUPQW3ddRw0mtlQE0iCJMdjq/d/O8Gywk0iHcdMi9dBczrUldPWJCxeJwpR omriTpgt62z19WVuuWnCvoeUmZvlCoi8uIhyZmF9PbEgazMTv3E1DjjtbO88ZT+sBWoh 5BnYky4fZ3iLnAtHTu3F/AN5TCYTqYEpoSCLRhVv8y9u+PXPzkrAdx6/VnSKtbWsrM2d d5NCdXZKx7+usnpRVdgiOV5BWg/YlANyRY1BBUiJTD4sjMmcVYgp64EtWaYQSXFD3Opi knFPAHXrHrz/bMkMs9WDf4P9EaSDdFQBYdQXulHiCFmmzw8smxa5g+q8wPYfmxoQlDzl xp5w== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AHQUAub7urS1wz/VlltNogu8xAjMyBeQDvDOXgs0VJuWsqvrE1sKG1yU yB9Nd5ecoihDdDT3W5FqZGE= X-Google-Smtp-Source: AHgI3Iaw/VLl4H5FICLBxvU0CE+jQQnI6DUPMKT9yQmJ9KUa9z8pr3mVw1blbetAPqWcalpt8ZQn4A== X-Received: by 2002:a63:2b84:: with SMTP id r126mr64742pgr.2.1549699506668; Sat, 09 Feb 2019 00:05:06 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a63:151d:: with SMTP id v29ls2933418pgl.2.gmail; Sat, 09 Feb 2019 00:05:06 -0800 (PST) X-Received: by 2002:a63:221f:: with SMTP id i31mr1202804pgi.47.1549699506240; Sat, 09 Feb 2019 00:05:06 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1549699506; cv=none; d=google.com; s=arc-20160816; b=xAXar+bk6ojTGA6KR9IVQ+kM+RgWxkYe5GKpO3pBpwL53ZkmgdiqlvObrZanhmNMuC amVb4f/Oz3mrI6pS2eq8a1B5Nwy0+p5J+tMYW/ZEZMwQAEka6eiulablzi5OUGTHUdXK zlfXGhaV9SKIR66jpfKSZfDYGNoo0VEZKvd6DooQhRmRuNHM3D1SYhCZfQ/nbXIjJ5f/ DaEUpBWX35nfL3FJ0DqgSxqTM7NtumSYhkA6rc6BR1JvXm0vkhorjBzmwa2UXyBDF637 KP/EQ4Zb0IsnZI1uHZD8cBC6HBGsCG7aH8U8pISAR3mxBPh5rxrcSdYteSmIUDntRoiD DEFg== 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:in-reply-to:references :mime-version:dkim-signature; bh=2YkAHXnVzi0RMVgxAUip1BCahz9518DYIoFT68Z+ARQ=; b=lpGRfYcqedcA2vxWZMrj7QSqUVHlHhhfZl24kzgSRaeAf61cfsXe3LNxSShkh+Yy2v /0Y06aRT/shxzJdQFD39eZIlf+6AuouD9XfgLZQHkRd0XNLD4BR61HLbketyaoCx/V2B PqfTT5faMsIAH+nN8ExlZgQJs1NCOtMTHbTMb9azOI+BOtphUK6Hpvu/mAsLhNZ4sc09 FXkhSYMjg5uTpfjebBOVhkCLU80fTWOJBSij4rc1YWvnJzGF5BZJXsyHDUk6FaeQRe2F IwWH3aG9xmVvbadNWJUF28tgNOlimhOMvDRRKHM9aKdBINONGsqTx38v5FKcpKNNO2jj Eynw== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b="UwPK/DIj"; spf=pass (google.com: domain of valery.isaev@gmail.com designates 2607:f8b0:4864:20::12a as permitted sender) smtp.mailfrom=valery.isaev@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-it1-x12a.google.com (mail-it1-x12a.google.com. [2607:f8b0:4864:20::12a]) by gmr-mx.google.com with ESMTPS id g97si236878plb.1.2019.02.09.00.05.06 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Sat, 09 Feb 2019 00:05:06 -0800 (PST) Received-SPF: pass (google.com: domain of valery.isaev@gmail.com designates 2607:f8b0:4864:20::12a as permitted sender) client-ip=2607:f8b0:4864:20::12a; Received: by mail-it1-x12a.google.com with SMTP id c9so15000160itj.1 for ; Sat, 09 Feb 2019 00:05:06 -0800 (PST) X-Received: by 2002:a5e:8417:: with SMTP id h23mr7437606ioj.183.1549699505512; Sat, 09 Feb 2019 00:05:05 -0800 (PST) MIME-Version: 1.0 References: <1a3dfba4-816a-42c3-8eea-1a2906cb1cad@googlegroups.com> In-Reply-To: From: Valery Isaev Date: Sat, 9 Feb 2019 11:04:29 +0300 Message-ID: Subject: Re: [HoTT] Re: Why do we need judgmental equality? To: Nicolai Kraus Cc: Homotopy Type Theory Content-Type: multipart/alternative; boundary="00000000000088ead20581718825" X-Original-Sender: valery.isaev@gmail.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b="UwPK/DIj"; spf=pass (google.com: domain of valery.isaev@gmail.com designates 2607:f8b0:4864:20::12a as permitted sender) smtp.mailfrom=valery.isaev@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.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: , --00000000000088ead20581718825 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Hi Nicolai, The notion of a conservative extension is certainly related to the notion of an equivalence of type theories that I'm referring to (I call it Morita equivalence). Hofmann defines various properties of the interpretation |-| : ITT -> ETT, which are weaker than Morita equivalence in general. The statement of Theorem 3.2.5 is almost equivalent to the notion of Morita equivalence. We just need to replace "|P'| =3D P" with "|P'| and P are propositionally equivalent" and add the condition that, for every \Gamma |-_I and every |\Gamma| |-_E A there is a type \Gamma |-_I A' such that |A'| and A are equivalent in the sense of HoTT (the latter condition follows from Theorem 3.2.5 for ITT and ETT, but not for general type theories). Then we get precisely the notion of Morita equivalence between type theories I and E. Regards, Valery Isaev =D1=81=D0=B1, 9 =D1=84=D0=B5=D0=B2=D1=80. 2019 =D0=B3. =D0=B2 04:41, Nicola= i Kraus : > Hi Valery, > > On Fri, Feb 8, 2019 at 11:32 PM Valery Isaev > wrote: > >> Now, what do I mean when I say that type theories T and Q(T) are >> equivalent? I won't give here the formal definition >> > > Would it be correct to say that T is a conservative extension of T, in th= e > sense of Martin Hofmann's thesis? Your description sounds a bit like this= , > or do you have something different in mind? > Nicolai > > > >> , but the idea is that Q(T) can be interpreted in T and, for every type = A >> of T, there is a type in Q(T) equivalent to A in T and the same is true = for >> terms. This implies that every statement (i.e., type) of Q(T) is provabl= e >> in Q(T) if and only if it is provable in T and every statement of T has = an >> equivalent statement in Q(T), so the theories are "logically equivalent"= . >> Moreover, equivalent theories have equivalent (in an appropriate >> homotopical sense) categories of models. >> >> Regards, >> Valery Isaev >> >> >> =D1=81=D0=B1, 9 =D1=84=D0=B5=D0=B2=D1=80. 2019 =D0=B3. =D0=B2 00:19, Mar= t=C3=ADn H=C3=B6tzel Escard=C3=B3 < >> escardo.martin@gmail.com>: >> >>> I would also like to know an answer to this question. It is true that >>> dependent type theories have been designed using definitional equality. >>> >>> But why would anybody say that there is a *need* for that? Is it >>> impossible to define a sensible dependent type theory (say for the purp= ose >>> of serving as a foundation for univalent mathematics) that doesn't ment= ion >>> anything like definitional equality? If not, why not? And notice that I= am >>> not talking about *usability* of a proof assistant such as the *existin= g* >>> ones (say Coq, Agda, Lean) were definitional equalities to be removed. = I >>> don't care if such hypothetical proof assistants would be impossibly >>> difficult to use for a dependent type theory lacking definitional >>> equalities (if such a thing exists). >>> >>> The question asked by Felix is a very sensible one: why is it claimed >>> that definitional equalities are essential to dependent type theories? >>> >>> (I do understand that they are used to compute, and so if you are >>> interested in constructive mathematics (like I am) then they are useful= . >>> But, again, in principle we can think of a dependent type theory with n= o >>> definitional equalities and instead an existence property like e.g. in >>> Lambek and Scott's "introduction to higher-order categorical logic". An= d >>> like was discussed in a relatively recent message by Thierry Coquand in >>> this list,) >>> >>> Martin >>> >>> >>> 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 coul= d, in >>>> principle, replace substitution along judgmental equality with explici= t >>>> transports if one added a few sensible rules to the type theory. Is th= ere a >>>> fundamental reason why the equality judgment is still necessary? >>>> >>>> Thanks, >>>> Felix Rech >>>> >>> -- >>> 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 HomotopyTypeTheory+unsubscribe@googlegroups.com. >>> For more options, visit https://groups.google.com/d/optout. >>> >> -- >> 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 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. --00000000000088ead20581718825 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Hi Nicolai,

The notion of a = conservative extension is certainly related to the notion of an equivalence= of type theories that I'm referring to (I call it Morita equivalence).= Hofmann defines various properties of the interpretation |-| : ITT -> E= TT, which are weaker than Morita equivalence in general. The statement of T= heorem 3.2.5 is almost equivalent to the notion of Morita equivalence. We j= ust need to replace "|P'| =3D P" with "|P'| and P ar= e propositionally equivalent" and add the condition that, for every \G= amma |-_I and every |\Gamma| |-_E A there is a type \Gamma |-_I A' such= that |A'| and A are equivalent in the sense of HoTT (the latter condit= ion follows from Theorem 3.2.5 for ITT and ETT, but not for general type th= eories). Then we get precisely the notion of Morita equivalence between typ= e theories I and E.

Regards,
Valery Isaev


=D1=81=D0=B1, 9 =D1=84=D0=B5=D0=B2=D1=80. 2019 =D0= =B3. =D0=B2 04:41, Nicolai Kraus <nicolai.kraus@gmail.com>:
Hi Valery,
On = Fri, Feb 8, 2019 at 11:32 PM Valery Isaev <valery.isaev@gmail.com> wrote:
Now, = what do I mean when I say that type theories T and Q(T) are equivalent? I w= on't give here the formal definition

<= div>Would it be correct to say that T is a conservative extension of T, in = the sense of Martin Hofmann's thesis? Your description sounds a bit lik= e this, or do you have something different in mind?
Nicolai
=

=C2=A0
, but the idea is that Q(T) can be interpreted in T= and, for every type A of T, there is a type in Q(T) equivalent to A in T a= nd the same is true for terms. This implies that every statement (i.e., typ= e) of Q(T) is provable in Q(T) if and only if it is provable in T and every= statement of T has an equivalent statement in Q(T), so the theories are &q= uot;logically equivalent". Moreover, equivalent theories have equivale= nt (in an appropriate homotopical sense) categories of models.
Regards,
Valery Isaev


<= div dir=3D"ltr" class=3D"gmail_attr">=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 <escardo.martin@= gmail.com>:
I would also like to know an answer to this question. I= t is true that dependent type theories have been designed using definitiona= l equality.

But why would anybody say that there is a *n= eed* for that? Is it impossible to define a sensible dependent type theory = (say for the purpose of serving as a foundation for univalent mathematics) = that doesn't mention anything like definitional equality? If not, why n= ot? And notice that I am not talking about *usability* of a proof assistant= such as the *existing* ones (say Coq, Agda, Lean) were definitional equali= ties to be removed. I don't care if such hypothetical proof assistants = would be impossibly difficult to use for a dependent type theory lacking de= finitional equalities (if such a thing exists).

Th= e question asked by Felix is a very sensible one: why is it claimed that de= finitional equalities are essential to dependent type theories?
<= br>
(I do understand that they are used to compute, and so if you= are interested in constructive mathematics (like I am) then they are usefu= l. But, again, in principle we can think of a dependent type theory with no= definitional equalities and instead an existence property like e.g. in Lam= bek and Scott's "introduction to higher-order categorical logic&qu= ot;. And like was discussed in a relatively recent message by Thierry Coqua= nd in this list,)

Martin=C2=A0


O= n 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 equa= lity 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?

Thanks,
Felix Rech

--
You received this message because you are subscribed to the G= oogle Groups "Homotopy Type Theory" group.
To unsubscribe from= this group and stop receiving emails from it, send an email to H= omotopyTypeTheory+unsubscribe@googlegroups.com.
For more options, vi= sit https:= //groups.google.com/d/optout.

--
You received this message because you are subscribed to the G= oogle Groups "Homotopy Type Theory" group.
To unsubscribe from= this group and stop receiving emails from it, send an email to H= omotopyTypeTheory+unsubscribe@googlegroups.com.
For more options, vi= sit https:= //groups.google.com/d/optout.

--
You received this message because you are subscribed to the Google Groups &= quot;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 http= s://groups.google.com/d/optout.
--00000000000088ead20581718825--