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-lj1-x23b.google.com (mail-lj1-x23b.google.com [IPv6:2a00:1450:4864:20::23b]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 2d8b8b73 for ; Sat, 9 Feb 2019 01:41:39 +0000 (UTC) Received: by mail-lj1-x23b.google.com with SMTP id v27-v6sf1462612ljv.1 for ; Fri, 08 Feb 2019 17:41:39 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1549676499; cv=pass; d=google.com; s=arc-20160816; b=Hh50+CXKa4g/DN6yL0HZKMD2gY+rad/yUlKNiR15AoDjlWCdBRXxl2FyvzmuclSAdW MmLO5iVL5f3/juOjZh6+XUyYPvnokRFdB5YOG1jCyX5R4DHqLxbxntg2T9yKQDdaZsal Rt6EjGJ/VzwZxPRyVnPCD6odwFBu9lNVJrLl2zV7YCVn7ym1Mc9BIN+ZdUZxGBXHlp1I 1G/R7Mb0hnbWDzPLReYwkv2FieeYaJQb05Haycnkmww56/etuhucsWmaZJczzqXVMxP+ jr1ZzHg6k+TcN61k6K7KgIYRCCoPGf24sElfPcux0asiIdARMxts83gfGiDVU+d9wYgc DJEw== 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=0OiD0tV2sVQa/5wA3UF35Osbsl3v/G29qW9oF1SVan0=; b=hMIkA0hBBJcy5D9HjQXAtP4knJuNPsY4GTdhGR1TQH03kEUbTtL4QbuUoKl8h9ybhj aSNcmXjN6yDVclDuGbpjNhHL80AbD0ZEx2AIgQog1I6A7i2YhQFztxpO5cLIhactXQpA KjHl5RHfwKHF6cdrLUMqXFbaztSpF86A6hL3ScwSjQYPU8vVsEk0k65Mm0agr3ZGtANc pXHb4h9vcJa8vrnGlRu1h67v5WuEUE+LDFjH85H9zPx7JzS9C560BPuMcapf1FAmS3g8 L+sdC3AFnWq4J0iP1TS8jotft18EUH80F2j33o3UarP/FinbdmSjUicOjr5Ogd2YF7C8 P8dg== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=mdmhaM4q; spf=pass (google.com: domain of nicolai.kraus@gmail.com designates 2a00:1450:4864:20::22e as permitted sender) smtp.mailfrom=nicolai.kraus@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=0OiD0tV2sVQa/5wA3UF35Osbsl3v/G29qW9oF1SVan0=; b=bL6bgv0FnfbXMg70zXJOryvD1Qmri/ClbkPoNzD9VncfAEloeYEDi2tlbWYWUMekwq H4KzaLnEV36coAQPx1CfsHT4OKjika5HFqzimyyz7dH6r6pxPByYtoYA/QpasPFGQkQO iLXHmGaWaG3SXdPUCVYgyfp4O7R6AyGphENUfQVQYKlJ67rS9OeLBn7yMGCHgmOOgED4 tJS7ewFW64Ly2gj4oLWZO1WvBoiM0bk4139USwQRMa0OfzUpNMGXpIHQSjXUkFEsot21 xxSO8XrWqA4REUmR0eovHg0zVNe+lmZUgbhLorcbl6XqOCvMP4q0uWwQB9RV9O8zky1w JuEw== 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=0OiD0tV2sVQa/5wA3UF35Osbsl3v/G29qW9oF1SVan0=; b=n8aS/JFKA5G/g7zdLVKw9ocYAQOftQbqrOIxDn6nXu6WBXQW/9+fpsDwmabYmun+1K CLlirMNC4grJr/4Adm/RZT7AHeMzpzXgSnOGXj47PaabQd93imY12J1Z4XNuwTnkD6FA TUh5M46t5lMHRxbVd+iNtySmPBQIpRXfGVP2bbPlRh5XOobDWJpRFhxHZEeIvdiKWrz6 +UCL9eRppDeT68iSxwLfM9Fl0GxA3hqO33atG2Qb9bD9cr5hcV2J4Fa/5ng3uTyY4XAI 60mkUjYXgFkuJ2b7oajn42adh76oUP0B/FsqY7+jBf6ztEt1023sQyILXXXS4hm3uifQ eeuA== 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=0OiD0tV2sVQa/5wA3UF35Osbsl3v/G29qW9oF1SVan0=; b=iG9b5OBE7xtn0B1J6+eRBrgk7UTJAkViXafz5hKLoUtiVaNF0GLw8oqpSPElhiB9oU IWDpE8uyvnKj+5AvUm2uubAIdgUdSl019eoBkUDMlAMv5unsCt7ooa57hHw71lCZ3jsa E2KYHgbBYCn1He2+p1A2j/UEigiLQp5RJpr2feyxIIIJQh4UbbVL3UGkfTH+Wy+QQZ/b a5ubafsaDLADEubhRSkEMJ/faTtN7zR3v1gSRvRx5CKY0e+/94vnRJ5T0TFlZ1vAtdfM 4hkHTIYj9WJ7PeuvXZL7rUSGx3aQEjdKAcOEaQAEB3UvinfITpUWEekQV0utAAtSmLPi EhtQ== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AHQUAubkc/jyltLhiDnW4rSlYykVsWvU71jRythRBmQTAaJB7nSZRZ4E j5r/CcPnhHmfpyHzC02o0J4= X-Google-Smtp-Source: AHgI3IZQPU46gZ3TH7+fI8czqxuJ7YcbJWQEljW0/C16ZB/oWjYXkcqcSqsTX4nTyp4bOU4eutGqqw== X-Received: by 2002:ac2:421a:: with SMTP id y26mr110778lfh.0.1549676498866; Fri, 08 Feb 2019 17:41:38 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a2e:95cc:: with SMTP id y12-v6ls612695ljh.14.gmail; Fri, 08 Feb 2019 17:41:38 -0800 (PST) X-Received: by 2002:a2e:9109:: with SMTP id m9-v6mr537850ljg.19.1549676498087; Fri, 08 Feb 2019 17:41:38 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1549676498; cv=none; d=google.com; s=arc-20160816; b=z5JkRogaruaxxQqzw8lub6h/HZa4FLW+RYGBZZ2i8eLMvX1/9trTMHnTLM0FzF9yR+ f+6qOceZTwtFrdE9h0jf+KSnjxwYUYF7WETH+Qpm6NjfQQf0yTtU/gbjkyEsILXj5SZS U3DP17PBwbIX3kMbMzDeUiNTz0jw/Go1EiPClycETi7IKK4nIBWmDGvHz5TcVWCN4pRN 6VzCe80bURpbceTgFqoWE5JRjhtLjxvcuF+zuYT7x8lR4IWrrwRfL4YQVmTJKj4W/DEH /Wr+UodnU9MVokS7Rq551YPTV5Ic9I/oq4uvyJoDyqQFwnnN1o6aUAumIYealIcJvUg0 QSNQ== 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=NLptDOfZzlNWVrPIBsaCee8oQlu/BVLYs14ob8P83L8=; b=CXxWUoC6To/dqHNQFjRxdbo/uiuaQitfEcL1L9FE5jzNrlWTUYDBzSAJ8Ma5xIlbg2 UZgXj7AsEPrRG+3igALBNH8LQgsylRpgB826ApwgKVCHMl6qWzFQGq9oB8FIGiyt1ZVH DtUgrGmbK3FE0KEM46a+t3pnenHqlbkmVAy59ak99RQRXG2/39561NPJP0s9Fp905T4Z Aw7MMHPumJ5lwrDuaXzlFcl6WfX6WIbyC5OChRlcQO5Gdd43wuOPNbA6ZkHEW98Khn0a SJVezGBeZFIl0/SlFQxO+kmLuOS1ri0Slrw82jgHjQ+ie/lezfUfgHfMQVShV7uT4DQd A9Yg== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=mdmhaM4q; spf=pass (google.com: domain of nicolai.kraus@gmail.com designates 2a00:1450:4864:20::22e as permitted sender) smtp.mailfrom=nicolai.kraus@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-lj1-x22e.google.com (mail-lj1-x22e.google.com. [2a00:1450:4864:20::22e]) by gmr-mx.google.com with ESMTPS id t16-v6si117481ljc.1.2019.02.08.17.41.38 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Fri, 08 Feb 2019 17:41:38 -0800 (PST) Received-SPF: pass (google.com: domain of nicolai.kraus@gmail.com designates 2a00:1450:4864:20::22e as permitted sender) client-ip=2a00:1450:4864:20::22e; Received: by mail-lj1-x22e.google.com with SMTP id c19-v6so4549334lja.5 for ; Fri, 08 Feb 2019 17:41:38 -0800 (PST) X-Received: by 2002:a2e:8196:: with SMTP id e22-v6mr7097649ljg.94.1549676497735; Fri, 08 Feb 2019 17:41:37 -0800 (PST) MIME-Version: 1.0 References: <1a3dfba4-816a-42c3-8eea-1a2906cb1cad@googlegroups.com> In-Reply-To: From: Nicolai Kraus Date: Sat, 9 Feb 2019 01:41:26 +0000 Message-ID: Subject: Re: [HoTT] Re: Why do we need judgmental equality? To: Valery Isaev Cc: Homotopy Type Theory Content-Type: multipart/alternative; boundary="0000000000002a168c05816c2dcf" X-Original-Sender: nicolai.kraus@gmail.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=mdmhaM4q; spf=pass (google.com: domain of nicolai.kraus@gmail.com designates 2a00:1450:4864:20::22e as permitted sender) smtp.mailfrom=nicolai.kraus@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: , --0000000000002a168c05816c2dcf Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable 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 the 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 f= or > terms. This implies that every statement (i.e., type) of Q(T) is provable > in Q(T) if and only if it is provable in T and every statement of T has a= n > 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, Mart= =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 purpo= se >> of serving as a foundation for univalent mathematics) that doesn't menti= on >> anything like definitional equality? If not, why not? And notice that I = am >> not talking about *usability* of a proof assistant such as the *existing= * >> 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 no >> definitional equalities and instead an existence property like e.g. in >> Lambek and Scott's "introduction to higher-order categorical logic". And >> 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 could= , in >>> principle, replace substitution along judgmental equality with explicit >>> transports if one added a few sensible rules to the type theory. Is the= re a >>> fundamental reason why the equality judgment is still necessary? >>> >>> Thanks, >>> Felix Rech >>> >> -- >> 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. >> > -- > 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. > --=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. --0000000000002a168c05816c2dcf Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Hi Valery,

On Fri, Feb 8, 2019 at 11:32 PM Valery Isae= v <valery.isaev@gmail.com&= gt; wrote:
Now, what do I mean when I say that type theories T and Q(T) ar= e equivalent? I won't give here the formal definition

Would it be correct to say that T is a conservative ex= tension of T, in the sense of Martin Hofmann's thesis? Your description= sounds a bit like this, or do you have something different in mind?
<= div>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) equiv= alent to A in T and the same is true for terms. This implies that every sta= tement (i.e., type) of Q(T) is provable in Q(T) if and only if it is provab= le in T and every statement of T has an equivalent statement in Q(T), so th= e theories are "logically equivalent". Moreover, equivalent theor= ies have equivalent (in an appropriate homotopical sense) categories of mod= els.

Regards,
<= div dir=3D"ltr">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 li= ke to know an answer to this question. It is true that dependent type theor= ies 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 purpose of serving as = a foundation for univalent mathematics) that doesn't mention anything l= ike definitional equality? If not, why not? And notice that I am not talkin= g about *usability* of a proof assistant such as the *existing* ones (say C= oq, 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).

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 mat= hematics (like I am) then they are useful. But, again, in principle we can = think of a dependent type theory with no definitional equalities and instea= d an existence property like e.g. in Lambek and Scott's "introduct= ion to higher-order categorical logic". And like was discussed in a re= latively recent message by Thierry Coquand in this list,)

Martin=C2=A0


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 s= eems to me like one could, in principle, replace substitution along judgmen= tal 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.
--0000000000002a168c05816c2dcf--