From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 2002:a25:bacd:: with SMTP id a13mr20874600ybk.461.1589138303041; Sun, 10 May 2020 12:18:23 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a25:748b:: with SMTP id p133ls2697985ybc.0.gmail; Sun, 10 May 2020 12:18:21 -0700 (PDT) X-Received: by 2002:a25:cf12:: with SMTP id f18mr21384627ybg.69.1589138301524; Sun, 10 May 2020 12:18:21 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1589138301; cv=none; d=google.com; s=arc-20160816; b=tzzmSDMyWSsGSlwTIJcpuohvHMeVlxIk/VP00GVBHE6WuvQLRYrer9tX1hrP+foOlQ B6KHfIKe2y2PlbW+pVCMiA6+l4LbQ4JGTBstmpqthGQeSZas74VskUw5MMqWXq0bzSYY UCrjn0j4aJIg0DmmBa4qCw3wyNZkj08VdH0Ju1lBnM+/DDsWD2akgq9/f8FNUHSNRcuc AKFRt+YlSrfc7dN4MbfGq1IYUyh66Tb1umS1KAH7L5LyO91QaA96kfn7miuG3rG+yBjK NNy6iis+PjnPeYEG/QoPz7j0quB6V6ZyU3fpMTa6J08XPRTCMcAMgGyRUjB38AWYwcdc YzsQ== 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=tnIRsThZlfc+M15w4r/8OcJXhQFSQlsHB1rjwGDqhC8=; b=jwrIJgLPMaCpJ4v9aG+EvmgTkNtEyZL0zXYmfEL7RGvu2lPJt6DVRNT8GdbYK31IcA dEKH5mb/TFd2TKHmG9I1IYHhlqwWyB20ywlHTHoEPF/20PmRy0L/AXIvJn/uu2jwGj8s 2NGd61ZY8KgJFOk4eBfkx+pE5DjtvP77Hnt7pYjoNmvGqlfl+nXquN4+os7Bwazb52Qs QBiANAJW8JeXPZ6MZMLq/EvnhUL7uYoaVCAuO0xk4FFQnsSGIdIZdCimz37y/as+hb11 nQ7i2PH9XO8nAUOZWK4UrAmEjFI//jGR7rsla5HEpNWdsf/X/l9/PmGjQ9iMdOxzIvtK P38A== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=NqoDph5M; spf=pass (google.com: domain of nicola...@gmail.com designates 2607:f8b0:4864:20::230 as permitted sender) smtp.mailfrom=nicola...@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Return-Path: Received: from mail-oi1-x230.google.com (mail-oi1-x230.google.com. [2607:f8b0:4864:20::230]) by gmr-mx.google.com with ESMTPS id y199si644648ybe.2.2020.05.10.12.18.21 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Sun, 10 May 2020 12:18:21 -0700 (PDT) Received-SPF: pass (google.com: domain of nicola...@gmail.com designates 2607:f8b0:4864:20::230 as permitted sender) client-ip=2607:f8b0:4864:20::230; Authentication-Results: gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=NqoDph5M; spf=pass (google.com: domain of nicola...@gmail.com designates 2607:f8b0:4864:20::230 as permitted sender) smtp.mailfrom=nicola...@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: by mail-oi1-x230.google.com with SMTP id 19so13299202oiy.8 for ; Sun, 10 May 2020 12:18:21 -0700 (PDT) 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; bh=tnIRsThZlfc+M15w4r/8OcJXhQFSQlsHB1rjwGDqhC8=; b=NqoDph5MMci5BErCFI2hDc5R9VTJ2R5cNIFi4Nkj8TwWjjCgsZ20K8oYxfTXPt3oYO Djoc8IziJ7C3uU/Z7wVSavQ888WSiTuYbpWHqNF3yT4XUK8fJVka0msdi6jOKy8+Syze O0n0jXDnRKH4AD5ClbEe5gMRqGARdy8xidYPg1nVSzs3L1P5+1RJX56Ip1ofVUPGBWMs uL8woR52vNMFCH7TT3ie4ArjDTUpKMLHg+Fng0sAWm9FOgQwm+chgQtgl1b/vTRauhXL hkjCLwT0VPAFOObBGfGVaOEceIJpnjRmiy9WPI6Md/SF2bQXqFC+l98gdVZL9M87b6wa SDnw== X-Gm-Message-State: AGi0PubIfBkuubmucYXzSI4gkueEjLcQSga0xyPgVQ5r27Xa6zI7lScd sAS9vlNDeFbor8T1fExIRHFYHmgO1VjG1tB/22njzyinOOo= X-Received: by 2002:aca:5614:: with SMTP id k20mr17284062oib.30.1589138301244; Sun, 10 May 2020 12:18:21 -0700 (PDT) MIME-Version: 1.0 References: <67E9DCCA-F9CA-45B7-9AC8-E5A7E94FE9A9@nottingham.ac.uk> <20200507100930.GA9390@mathematik.tu-darmstadt.de> <8C57894C7413F04A98DDF5629FEC90B1652F5334@Pli.gst.uqam.ca> <8C57894C7413F04A98DDF5629FEC90B1652F53A3@Pli.gst.uqam.ca> <20200508064039.GC21473@mathematik.tu-darmstadt.de> <8C57894C7413F04A98DDF5629FEC90B1652F54CC@Pli.gst.uqam.ca> <20200509082829.GA8417@mathematik.tu-darmstadt.de> <8C57894C7413F04A98DDF5629FEC90B1652F55C8@Pli.gst.uqam.ca> <20200509184313.GB28841@mathematik.tu-darmstadt.de> <8C57894C7413F04A98DDF5629FEC90B1652F563A@Pli.gst.uqam.ca> In-Reply-To: From: Nicolai Kraus Date: Sun, 10 May 2020 20:18:09 +0100 Message-ID: Subject: Re: [HoTT] Identity versus equality To: =?UTF-8?Q?Joyal=2C_Andr=C3=A9?= , Thomas Streicher Cc: David Roberts , Thorsten Altenkirch , Michael Shulman , Steve Awodey , "homotopyt...@googlegroups.com" Content-Type: multipart/alternative; boundary="000000000000f1d78005a550174e" --000000000000f1d78005a550174e Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable In the last paragraph of my message below, the words "deep" and "shallow" have to be swapped. On Sun, May 10, 2020 at 5:51 PM Nicolai Kraus wrote: > Dear Andr=C3=A9 and everyone, > > I feel it's worth pointing out that there are two strategies to express > "everyday mathematics" in HoTT. In CS-speak, they would probably be > called "shallow embedding" and "deep embedding". Shallow embedding is > the "HoTT style", deep embedding is the "pre-HoTT type theory style". > Shallow means that one uses that the host language shares structure with > the object one wants to define, while deep means one doesn't. To explain > what I mean, let's look at the type theoretic definition of a group (a > 1-group, not a higher group). > > Definition using deep embedding: A group is a tuple > (X,h,e,o,i,assoc,...), where > X : Type -- carrier > h : is-0-truncated(X) -- carrier is set > e : X -- unit > o : X * X -> X -- composition > i : X -> X -- inverses > assoc : (h o g) o f =3D h o (g o f) > ... [and so on] > > Definition using shallow embedding: A group is a pointed connected 1-type= . > > Fortunately, these definitions are equivalent (via the Eilenberg-McLan > spaces construction). But they behave differently when we want to work > with them or change them. It's easy to change the second definition to > define infinity groups instead of 1-groups (see e.g. arXiv:1802.04315 , > arXiv:1805.02069, and Ulrik's comment). But it's unclear whether there > is a nice way for the first definition. The second definition has better > computational properties than the first. > > When you say this: > > > But I find it frustrating that I cant do my everyday mathematics with > it. > > For example, I cannot say > > > > (1) Let X:\Delta^{op}---->Type be a simplicial type; > > You are referring to shallow embedding. In everyday mathematics, you > don't say (1) either. You probably say (1) with "Type" replaced by "Set" > or by "simplicial set". Both of these can be expressed straightforwardly > in type theory using only (h-)sets (i.e. embedding deeply). > > We strive to use shallow embedding as often as possible for the reasons > in the above example. But let's assume that we *can* say (1) in HoTT, > using "Type", because we find some encoding that we're reasonably happy > with; there's a question which I've asked myself before: > > Will we not destroy the advantages of deep (over shallow) embedding if > we fall back to encodings (and thus destroy the main selling point of > HoTT)? For me, the justification of still using deep embedding is that > statements using encodings (e.g. "the universe is a higher category) > might still imply statements which don't use encodings and are > interesting. However, if we want to develop a theory of certain higher > structures for it's own sake, then it's not so clear to me whether it's > really better to use the HoTT-style deep embedding. > > Kind regards, > Nicolai > > > On 09/05/2020 21:18, Joyal, Andr=C3=A9 wrote: > > Dear Thomas, > > > > You wrote > > > > < > for proving and not for computing. > > But if you haven't mechanized PART of equational reasoning it would be > > much much more painful than it still is. > > But that is "only" a pragmatic issue.>> > > > > Type theory has very nice features. I wish they could be preserved and > developped further. > > But I find it frustrating that I cant do my everyday mathematics with i= t. > > For example, I cannot say > > > > (1) Let X:\Delta^{op}---->Type be a simplicial type; > > (2) Let G be a type equipped with a group structure; > > (3) Let BG be the classifying space of a group G; > > (4) Let Gr be the category of groups; > > (5) Let SType be the category of simplical types. > > (6) Let Map(X,Y) be the simplicial types of maps X--->Y > > between two simplicial types X and Y. > > > > It is crucial to have (1) > > For example, a group could be defined to > > be a simplicial object satisfying the Segal conditions. > > The classifying space of a group is the colimit of this simplicial > object. > > The category of groups can be defined to be > > a simplicial objects satisfiying the Rezk conditions (a complete Segal > space). > > > > Is there some aspects of type theory that we may give up as a price > > for solving these problems ? > > > > > > Best, > > Andr=C3=A9 > > > > ________________________________________ > > From: Thomas Streicher [stre...@mathematik.tu-darmstadt.de] > > Sent: Saturday, May 09, 2020 2:43 PM > > To: Joyal, Andr=C3=A9 > > Cc: David Roberts; Thorsten Altenkirch; Michael Shulman; Steve Awodey; > homotopyt...@googlegroups.com > > Subject: Re: [HoTT] Identity versus equality > > > > Dear Andr'e, > > > >> By the way, if type theory is not very effective in practice, why do w= e > insist that it should always compute? > >> The dream of a formal system in which every proof leads to an actual > computation may be far off. > >> Not that we should abandon it, new discoveries are always possible. > >> Is there a version of type theory for proving and verifying, less > >> for computing? > > In my opinion the currenrly implemented type theories are essentially > > for proving and not for computing. > > But if you haven't mechanized PART of equational reasoning it would be > > much much more painful than it still is. > > But that is "only" a pragmatic issue. > > > >> The notations of type theory are very useful in homotopy theory. > >> But the absence of simplicial types is a serious obstacle to > applications. > > In cubical type theory they sort of live well with cubes not being > > fibrant... They have them as pretypes. But maybe I misunderstand... > > > > Thomas > > > > --000000000000f1d78005a550174e Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
In the last paragraph of my message below, the words = "deep" and "shallow" have to be swapped.=C2=A0
On Sun, M= ay 10, 2020 at 5:51 PM Nicolai Kraus <nicola...@gmail.com> wrote:
Dear Andr=C3=A9 and everyone,

I feel it's worth pointing out that there are two strategies to express=
"everyday mathematics" in HoTT. In CS-speak, they would probably = be
called "shallow embedding" and "deep embedding". Shallo= w embedding is
the "HoTT style", deep embedding is the "pre-HoTT type theor= y style".
Shallow means that one uses that the host language shares structure with the object one wants to define, while deep means one doesn't. To explai= n
what I mean, let's look at the type theoretic definition of a group (a =
1-group, not a higher group).

Definition using deep embedding: A group is a tuple
(X,h,e,o,i,assoc,...), where
=C2=A0=C2=A0 X : Type=C2=A0=C2=A0=C2=A0=C2=A0 -- carrier
=C2=A0=C2=A0 h : is-0-truncated(X)=C2=A0=C2=A0=C2=A0=C2=A0 -- carrier is se= t
=C2=A0=C2=A0 e : X=C2=A0=C2=A0 -- unit
=C2=A0=C2=A0 o : X * X -> X=C2=A0=C2=A0=C2=A0=C2=A0 -- composition
=C2=A0=C2=A0 i : X -> X=C2=A0=C2=A0=C2=A0=C2=A0 -- inverses
=C2=A0=C2=A0 assoc : (h o g) o f =3D h o (g o f)
=C2=A0=C2=A0 ... [and so on]

Definition using shallow embedding: A group is a pointed connected 1-type.<= br>
Fortunately, these definitions are equivalent (via the Eilenberg-McLan
spaces construction). But they behave differently when we want to work
with them or change them. It's easy to change the second definition to =
define infinity groups instead of 1-groups (see e.g. arXiv:1802.04315 , arXiv:1805.02069, and Ulrik's comment). But it's unclear whether th= ere
is a nice way for the first definition. The second definition has better computational properties than the first.

When you say this:

=C2=A0> But I find it frustrating that I cant do my everyday mathematics= with it.
=C2=A0> For example, I cannot=C2=A0 say
=C2=A0>
=C2=A0> (1) Let X:\Delta^{op}---->Type be a simplicial type;

You are referring to shallow embedding. In everyday mathematics, you
don't say (1) either. You probably say (1) with "Type" replac= ed by "Set"
or by "simplicial set". Both of these can be expressed straightfo= rwardly
in type theory using only (h-)sets (i.e. embedding deeply).

We strive to use shallow embedding as often as possible for the reasons in the above example. But let's assume that we *can* say (1) in HoTT, <= br> using "Type", because we find some encoding that we're reason= ably happy
with; there's a question which I've asked myself before:

Will we not destroy the advantages of deep (over shallow) embedding if
we fall back to encodings (and thus destroy the main selling point of
HoTT)? For me, the justification of still using deep embedding is that
statements using encodings (e.g. "the universe is a higher category) <= br> might still imply statements which don't use encodings and are
interesting. However, if we want to develop a theory of certain higher
structures for it's own sake, then it's not so clear to me whether = it's
really better to use the HoTT-style deep embedding.

Kind regards,
Nicolai


On 09/05/2020 21:18, Joyal, Andr=C3=A9 wrote:
> Dear Thomas,
>
> You wrote
>
> <<In my opinion the currenrly implemented type theories are esse= ntially
> for proving and not for computing.
> But if you haven't mechanized PART of equational reasoning it woul= d be
> much much more painful than it still is.
> But that is "only" a pragmatic issue.>>
>
> Type=C2=A0 theory has very nice features. I wish they could be preserv= ed and developped further.
> But I find it frustrating that I cant do my everyday mathematics with = it.
> For example, I cannot=C2=A0 say
>
> (1) Let X:\Delta^{op}---->Type be a simplicial type;
> (2) Let G be a type equipped with a group structure;
> (3) Let BG be the classifying space of a group G;
> (4) Let Gr be the category of groups;
> (5) Let SType be the category of simplical types.
> (6) Let Map(X,Y) be the simplicial types of maps X--->Y
> between two simplicial types X and Y.
>
> It is crucial to have (1)
> For example, a group could be defined to
> be a simplicial object satisfying the Segal conditions.
> The classifying space of a group is the colimit of this simplicial obj= ect.
> The category of groups can be defined to be
> a simplicial objects satisfiying the Rezk conditions (a complete Segal= space).
>
> Is there some aspects of type theory that we may give up as a price > for solving these problems ?
>
>
> Best,
> Andr=C3=A9
>
> ________________________________________
> From: Thomas Streicher [stre...@mathematik.tu-darmstadt.de]
> Sent: Saturday, May 09, 2020 2:43 PM
> To: Joyal, Andr=C3=A9
> Cc: David Roberts; Thorsten Altenkirch; Michael Shulman; Steve Awodey;= homotop= yt...@googlegroups.com
> Subject: Re: [HoTT] Identity versus equality
>
> Dear Andr'e,
>
>> By the way, if type theory is not very effective in practice, why = do we insist that it should always compute?
>> The dream of a formal system in which every proof leads to an actu= al computation may be far off.
>> Not that we should abandon it, new discoveries are always possible= .
>> Is there a version of type theory for proving and verifying, less<= br> >> for computing?
> In my opinion the currenrly implemented type theories are essentially<= br> > for proving and not for computing.
> But if you haven't mechanized PART of equational reasoning it woul= d be
> much much more painful than it still is.
> But that is "only" a pragmatic issue.
>
>> The notations of type theory are very useful in homotopy theory. >> But the absence of simplicial types is a serious obstacle to appli= cations.
> In cubical type theory they sort of live well with cubes not being
> fibrant... They have them as pretypes. But maybe I misunderstand... >
> Thomas
>

--000000000000f1d78005a550174e--