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=-0.8 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-oi1-x23b.google.com (mail-oi1-x23b.google.com [IPv6:2607:f8b0:4864:20::23b]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 2e99ded4 for ; Tue, 26 Nov 2019 19:14:44 +0000 (UTC) Received: by mail-oi1-x23b.google.com with SMTP id j14sf9899196oie.1 for ; Tue, 26 Nov 2019 11:14:44 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:date:from:to:message-id:in-reply-to:references:subject :mime-version:x-original-sender:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=DBgooTccINV9M5a7Sa4Bjj/47WUf5vTpAwdq3hFptrY=; b=GD/gZh7GUDGJj69VPk4+JNGzBkpbAmJXkxUMFJ9fdyPgmY0FXMC5IAO/diWnLTLGCT rQQn0YPbymLlwEL6yewODdkwYem6CbKJt8Yfi5qBqMmkGkTIB/B5yQ++CyjyZoRnwp5n XlCP5zK6t7zKOEgHVXIHSm2P/SlI+THZ4xETWU/oYvUqXf1HFp1e4u5fOdoj+zO7k+FH wOcO3BkFUhqlY8KEYLO1FdMaEPTMwruj/fXTZ5jeufUrKhkh+Osb4mYJSCoXWUQL8KyX IICP3YMOHAdY0A/99nJUp1igGDFYlONPHzME47/HeDQliE8aBHAlrtRo45pIUj4/jImF JY/A== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=date:from:to:message-id:in-reply-to:references:subject:mime-version :x-original-sender:precedence:mailing-list:list-id:list-post :list-help:list-archive:list-unsubscribe; bh=DBgooTccINV9M5a7Sa4Bjj/47WUf5vTpAwdq3hFptrY=; b=OEKdozMd0Q/iffnseo1YYTYfNSSNlkXd7K/SVPAw9sLTgp/q99O6mVOZKm9+IwB+b2 Bh11g6RnvYPlP7eJVJLhH4noNAJtVYuM029Cn5KNlmhw9S3i7tFS9s9hNENrZHnCGZKP eHclB8GhPEjAO8sLsdzAtVNDkBmkYBv0On4XZeS/ZeFMLfSaLXYzvUL2/zH8BXFwfdvv ywT29fZMXOfdkBokWLxOSQ1sueiyiOFSJiJZr2M+ns7xLg4h1poW88hSr+Oy7O16sOoD Dycmucc2wv2gCR1elGwO/ynxb6HattGPOhPAVx1++MCBCKyjZulao3jrB/a35Ejg4jS9 t66Q== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:date:from:to:message-id:in-reply-to :references:subject:mime-version:x-original-sender:precedence :mailing-list:list-id:x-spam-checked-in-group:list-post:list-help :list-archive:list-unsubscribe; bh=DBgooTccINV9M5a7Sa4Bjj/47WUf5vTpAwdq3hFptrY=; b=Tqg51upX55PGzkQQ7a6Neao52ihpMtkzUlkHHLostTnY8aTOM3a6bqYRP35B1PZCfh Q8kmH9MWS574m7ObGZjVLNOiCvAj+IPz9yyf9gMGZ2gttUzZcOnA3/w4bH6qqEzDjai3 KVVkn42XTtuHLh+Lt3+AvH0Bvmi/D9I1d4HbqbrxdqlsNLK4cWvCZzXiL0mRD+G+Kfk1 gBAYa1Cg2eFEcbZDXjcSg4BgPzGGfBVwXmLNB1wOy90nKRGHHIN5ohwi/9eICudfd+K1 8zocrzusHVqxdGtt7xKHV6xD9bWDfzZEQuFY38aPWheau/t/0OsLuY/ABaZVvYp1BasG lhGw== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAW4G/yxokBZbV/5NhJUzI8ZReqeAYBOm3qlVXwcl/1X1FyaI3E/ ZHQUXP+Jc8wyHsUmfvA3ZG8= X-Google-Smtp-Source: APXvYqwzjGe3GMhTzDNGpoc+E9Cc02R3Rx7ulxkvHrUTtdeGsTCfO0Pk1GnD9gVWtrZ5iUmUEEGYJw== X-Received: by 2002:a05:6830:1d71:: with SMTP id l17mr448682oti.236.1574795683471; Tue, 26 Nov 2019 11:14:43 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:aca:d10:: with SMTP id 16ls3467465oin.7.gmail; Tue, 26 Nov 2019 11:14:43 -0800 (PST) X-Received: by 2002:a05:6808:644:: with SMTP id z4mr492113oih.139.1574795682683; Tue, 26 Nov 2019 11:14:42 -0800 (PST) Date: Tue, 26 Nov 2019 11:14:41 -0800 (PST) From: =?UTF-8?Q?Mart=C3=ADn_H=C3=B6tzel_Escard=C3=B3?= To: Homotopy Type Theory Message-Id: <13f496d9-1d01-4a2f-b5c1-826dd87aebf2@googlegroups.com> In-Reply-To: References: <2ca6c47c-6196-4b45-b82c-db79b2b6568c@googlegroups.com> Subject: Re: [HoTT] Why did Voevodsky find existing proof assistants to be 'impractical'? MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_1722_1204507170.1574795682018" X-Original-Sender: escardo.martin@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: , ------=_Part_1722_1204507170.1574795682018 Content-Type: multipart/alternative; boundary="----=_Part_1723_384125619.1574795682019" ------=_Part_1723_384125619.1574795682019 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable On Tuesday, 26 November 2019 00:25:37 UTC, Michael Shulman wrote: > > HoTT instead expands the notion of "equality" to=20 > essentially mean "isomorphism" and requires transporting along it as a=20 > nontrivial action. I doubt that that's what you have in mind, but=20 > maybe you could explain what you do mean?=20 > I think terminology and notation alone cause a lot of confusion (and I have said this many times in this list in the past, before Kevin joined in)= . Much of the disagreement is not a real disagreement but a misunderstanding. * In HoTT, or in univalent mathematics, we use the terminology "equals" and the notation "=3D" for something that is not the same notion as in "traditional mathematics". * Before the univalence axiom, we had Martin-Loef's identity type. * It was *intended* to capture equality *as used by mathematicians* (constructive or not). * But it didn't. Hofmann and Streicher proved that. * The identity type captures something else. It certainly doesn't capture truth-valued equality by default. In particular, Voevosdky showed that it captures isomorphism of sets, and more generality equivalence of =E2=88=9E-groupoids. But this is distorting history a bit. In the initial drafts of his "homotopy lambda calculus", he tried come up with a new construction in type theory to capture equivalence. It was only later that he found out that what he needed was precisely Martin-Loef's identity type. * So writing "x =3D y" for the identity type is a bit perverse. People may say, and they have said "but there is no other sensible notion of equality for such type theories. That may be so, but because, in any case, *it is not the same notion of equality*, we should not use the same symbol. * Similarly, writing "X =E2=89=83 Y" is a bit perverse, too. In truth-valued mathematics, "X =E2=89=83 Y" is most of the time intende= d to be truth-valued, not set-valued. (Exception: category theory. E.g. we write a long chain of isomorphisms to establish that two objects are isomorphic. Then we learn that the author of such a proof was not interested in the existence of an isomorphism, but instead to provide an example. Such a proof/construction is usually concluded by saying something like "by chasing the isomorphism, we see that we can take [...] as our desired isomorphism.) * With the above out of the way, we can consider the imprecise slogan "isomorphic types are equal". The one thing that the univalence axiom doesn't say is that isomorphic type are equal. What it does say is that the *identity type* Id X Y is in canonical bijection with the type X =E2=89=83 Y of equivalences. * What is the effect of this? - That the identity type behaves like isomorphism, rather than like equality. - And that isomorphism behaves a little bit like equality. The important thing above is "a little bit". In particular, we cannot *substitute* things by isomorphic things. We can only *transport* them (just like things work as usual with isomorphisms). * Usually, the univalence axioms is expressed as a relation between equality and isomorphism. Where by equality we don't mean equality but instead the identity type. A way to avoid these terminological problems is to formulate univalence as a property of isomorphisms, or more precisely equivalences. To show that all equivalences satisfy a given property, it is enough to prove that all the identity equivalence between any two types have this property. * So, as Mike says above, most of the time we can work with type equivalence rather than "type equality". And I do too. Something that is not well explained at all in the literature is when and how the univalence axiom *actually makes a difference*. (I guess this is not well understood. I used to thing that the univalence axioms makes a difference only for types that are not sets. But actually, for example, the univalence axiom is needed (in the absence of the K axiom) to prove that the type of ordinals is a set.) * One example: object classifiers, subtype classifiers, ... * Sometimes the univalence axiom may be *convenient* but *not needed*. I guess that Kevin is, in particular, saying precisely that. In all cases where he needs to transport constructions along isomorphisms, he is confident that this can be done without univalence. And I would agree with this assessment. Best, Martin =20 --=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. To view this discussion on the web visit https://groups.google.com/d/msgid/= HomotopyTypeTheory/13f496d9-1d01-4a2f-b5c1-826dd87aebf2%40googlegroups.com. ------=_Part_1723_384125619.1574795682019 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable


On Tuesday, 26 November 2019 00:25:37 UTC, Michael= Shulman wrote:
HoTT instead e= xpands the notion of "equality" to
essentially mean "isomorphism" and requires transporting alon= g it as a
nontrivial action. =C2=A0I doubt that that's what you have in mind,= but
maybe you could explain what you do mean?

=C2=A0I think terminology and notation= alone cause a lot of confusion (and I
have said this many times = in this list in the past, before Kevin joined in).

Much of the disagreement is not a real disagreement but a
misund= erstanding.

=C2=A0* In HoTT, or in univalent mathe= matics, we use the terminology
=C2=A0 =C2=A0"equals" an= d the notation "=3D" for something that is not the same
=C2=A0 =C2=A0notion as in "traditional mathematics".
<= br>
=C2=A0* Before the univalence axiom, we had Martin-Loef's= identity type.

=C2=A0* It was *intended* to captu= re equality *as used by mathematicians*
=C2=A0 =C2=A0(constructiv= e or not).

=C2=A0* But it didn't. Hofmann and = Streicher proved that.

=C2=A0* The identity type c= aptures something else.

=C2=A0 =C2=A0It certainly = doesn't capture truth-valued equality by default.

<= div>=C2=A0 =C2=A0In particular, Voevosdky showed that it captures isomorphi= sm of
=C2=A0 =C2=A0sets, and more generality equivalence of =E2= =88=9E-groupoids.

=C2=A0 =C2=A0But this is distort= ing history a bit.

=C2=A0 =C2=A0In the initial dra= fts of his "homotopy lambda calculus", he tried
=C2=A0 = =C2=A0come up with a new construction in type theory to capture
= =C2=A0 =C2=A0equivalence.

=C2=A0 =C2=A0It was only= later that he found out that what he needed was
=C2=A0 =C2=A0pre= cisely Martin-Loef's identity type.

=C2=A0* So= writing "x =3D y" for the identity type is a bit perverse.
=

=C2=A0 =C2=A0People may say, and they have said "b= ut there is no other sensible
=C2=A0 =C2=A0notion of equality for= such type theories.

=C2=A0 =C2=A0That may be so, = but because, in any case, *it is not the same
=C2=A0 =C2=A0notion= of equality*, we should not use the same symbol.

= =C2=A0* Similarly, writing "X =E2=89=83 Y" is a bit perverse, too= .

=C2=A0 =C2=A0In truth-valued mathematics, "= X =E2=89=83 Y" is most of the time intended
=C2=A0 =C2=A0to = be truth-valued, not set-valued.

=C2=A0 =C2=A0(Exc= eption: category theory. E.g. we write a long chain of
=C2=A0 =C2= =A0isomorphisms to establish that two objects are isomorphic. Then we
=
=C2=A0 =C2=A0learn that the author of such a proof was not interested = in the
=C2=A0 =C2=A0existence of an isomorphism, but instead to p= rovide an
=C2=A0 =C2=A0example. Such a proof/construction is usua= lly concluded by saying
=C2=A0 =C2=A0something like "by chas= ing the isomorphism, we see that we can take
=C2=A0 =C2=A0[...] a= s our desired isomorphism.)


=C2=A0*= With the above out of the way, we can consider the imprecise slogan
<= div>=C2=A0 =C2=A0"isomorphic types are equal".

=C2=A0 =C2=A0The one thing that the univalence axiom doesn't say= is that
=C2=A0 =C2=A0isomorphic type are equal.

=C2=A0 =C2=A0What it does say is that the *identity type* Id X Y i= s in canonical
=C2=A0 =C2=A0bijection with the type X =E2=89=83 Y= of equivalences.

=C2=A0* What is the effect of th= is?

=C2=A0 =C2=A0- That the identity type behaves = like isomorphism, rather than like
=C2=A0 =C2=A0 =C2=A0equality.<= /div>

=C2=A0 =C2=A0- And that isomorphism behaves a litt= le bit like equality.

=C2=A0 =C2=A0The important t= hing above is "a little bit".

=C2=A0 =C2= =A0In particular, we cannot *substitute* things by isomorphic
=C2= =A0 =C2=A0things. We can only *transport* them (just like things work as
=C2=A0 =C2=A0usual with isomorphisms).

=C2= =A0* Usually, the univalence axioms is expressed as a relation between
=C2=A0 =C2=A0equality and isomorphism.

=C2= =A0 =C2=A0Where by equality we don't mean equality but instead the iden= tity
=C2=A0 =C2=A0type.

=C2=A0 =C2=A0A w= ay to avoid these terminological problems is to formulate
=C2=A0 = =C2=A0univalence as a property of isomorphisms, or more precisely
=C2=A0 =C2=A0equivalences.

=C2=A0 =C2=A0To show t= hat all equivalences satisfy a given property, it is
=C2=A0 =C2= =A0enough to prove that all the identity equivalence between any two
<= div>=C2=A0 =C2=A0types have this property.

=C2=A0*= So, as Mike says above, most of the time we can work with type
= =C2=A0 =C2=A0equivalence rather than "type equality". And I do to= o.

=C2=A0 =C2=A0Something that is not well explain= ed at all in the literature is
=C2=A0 =C2=A0when and how the univ= alence axiom *actually makes a difference*.

=C2=A0= =C2=A0(I guess this is not well understood. I used to thing that the
=
=C2=A0 =C2=A0univalence axioms makes a difference only for types that = are not
=C2=A0 =C2=A0sets. But actually, for example, the univale= nce axiom is needed (in
=C2=A0 =C2=A0the absence of the K axiom) = to prove that the type of ordinals is a
=C2=A0 =C2=A0set.)
<= div>
=C2=A0 =C2=A0 =C2=A0 * One example: object classifiers, = subtype classifiers, ...

=C2=A0* Sometimes the uni= valence axiom may be *convenient* but *not needed*.

=C2=A0 =C2=A0I guess that Kevin is, in particular, saying precisely that.= In all
=C2=A0 =C2=A0cases where he needs to transport constructi= ons along isomorphisms,
=C2=A0 =C2=A0he is confident that this ca= n be done without univalence. And I
=C2=A0 =C2=A0would agree with= this assessment.

Best,
Martin


=C2=A0

--
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.
To view this discussion on the web visit https://groups.google.co= m/d/msgid/HomotopyTypeTheory/13f496d9-1d01-4a2f-b5c1-826dd87aebf2%40googleg= roups.com.
------=_Part_1723_384125619.1574795682019-- ------=_Part_1722_1204507170.1574795682018--