From mboxrd@z Thu Jan  1 00:00:00 1970
X-Received: by 2002:a9d:2426:: with SMTP id p35-v6mr9156843ota.49.1527606960026;
        Tue, 29 May 2018 08:16:00 -0700 (PDT)
X-BeenThere: homotopytypetheory@googlegroups.com
Received: by 2002:a9d:6187:: with SMTP id g7-v6ls597955otk.7.gmail; Tue, 29
 May 2018 08:15:57 -0700 (PDT)
X-Received: by 2002:a9d:3ed:: with SMTP id f100-v6mr9230002otf.65.1527606957780;
        Tue, 29 May 2018 08:15:57 -0700 (PDT)
ARC-Seal: i=1; a=rsa-sha256; t=1527606957; cv=none;
        d=google.com; s=arc-20160816;
        b=rHjYkYLCIQewKoNAMnFWb4Z410i+8dXwWsqEPOPfcpdT0vdUpyc6arP7TbihehvaZr
         ubD8napGtVE9dsvR7ldV4c1WuyfMyIyyvtEVTAe46mQT8rXJonEhwhHgrPThq+T1pUkG
         2N2rk+FpdEzbEus48fSACj/Wj4JSRIDPinkm4ndXY7HbQrFriJM57ahxO2lVMVLqDiI7
         xEKmvRy/b941PRlHxsrWs1IGNjchxb6YSUlH0glHjqxD09vhkAorUp44pOgvgBeaeLBX
         CUBzUvQUB0XW6zHnCfKRbzLD3QFnBcqDKDTLIpfnu0j4K1MTcpsaS1Fyd9c+hfD3cXgK
         S4iA==
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:references:in-reply-to
         :mime-version:dkim-signature:arc-authentication-results;
        bh=lRyebs2hcDmhdTPDPWuCAQUW1kMhMacqxRYCw85bekk=;
        b=z42FHWFULEghwS4l5Sk3QZj19xGhGQPFoWD6aM/bJhLNln61oh9fndrKiHvXe1lEDP
         7EblNm++K7F8XZfDgGkdcwoyWKXdzkbRroZOvFSG+ykYGI1nKXL+HAh7+Zadg+Dj3TAZ
         CzgWCZ8ym5maIsoX1OVE3pKjaYp/TuLBZIF9Ch+NIHSdb16PpRkQZn301Kp2/cLXE+ZW
         Zhu5d95uN32Ecl5bL3vnR+Zmx9SCT0++w3c5DNBqAzCtgo/xkImwcQB0KjMUAlsFT3m9
         y0PG1IyvtTX7GJEYKnIz4Gqd3IuYd1zb8rOeMWXFejDnvcEXCOCP9t9qhcXD03ma+eoY
         /pEQ==
ARC-Authentication-Results: i=1; gmr-mx.google.com;
       dkim=pass head...@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=pU7TqKtP;
       spf=neutral (google.com: 2607:f8b0:4002:c05::233 is neither permitted nor denied by domain of shu...@sandiego.edu) smtp.mailfrom=shu...@sandiego.edu
Return-Path: <shu...@sandiego.edu>
Received: from mail-yw0-x233.google.com (mail-yw0-x233.google.com. [2607:f8b0:4002:c05::233])
        by gmr-mx.google.com with ESMTPS id u13-v6si2464961oif.3.2018.05.29.08.15.57
        for <homotopyt...@googlegroups.com>
        (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128);
        Tue, 29 May 2018 08:15:57 -0700 (PDT)
Received-SPF: neutral (google.com: 2607:f8b0:4002:c05::233 is neither permitted nor denied by domain of shu...@sandiego.edu) client-ip=2607:f8b0:4002:c05::233;
Authentication-Results: gmr-mx.google.com;
       dkim=pass head...@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=pU7TqKtP;
       spf=neutral (google.com: 2607:f8b0:4002:c05::233 is neither permitted nor denied by domain of shu...@sandiego.edu) smtp.mailfrom=shu...@sandiego.edu
Received: by mail-yw0-x233.google.com with SMTP id q7-v6so4906911ywd.9
        for <homotopyt...@googlegroups.com>; Tue, 29 May 2018 08:15:57 -0700 (PDT)
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed;
        d=sandiego-edu.20150623.gappssmtp.com; s=20150623;
        h=mime-version:in-reply-to:references:from:date:message-id:subject:to
         :cc;
        bh=lRyebs2hcDmhdTPDPWuCAQUW1kMhMacqxRYCw85bekk=;
        b=pU7TqKtPdTPImtYzXRoCkDT6Um1kZZmmd3d9hLkgBuvG65AixQ7S0ZHjqHuChQWad5
         Tr4W/1rZrtRIfABPUzAYDBiF76DFu6fDpTZpC918SNisqqX88+BiGyiDNRiaXMAputiA
         nhBrC6i1IGZjmCJlAetS0h5eNWilVD+3DtvcLJ76Kd30pyuzlTQ5my6BsMy2sK7Ph8HE
         6Y5C2oTtvE4VtP3OU2lX0Al34anUJBcQxTa4SavOGBi1nZYHT9DX1AajjsSDWtvMLr2a
         HNNL0mr2n68dJTdYxNFhY2QQwsuSGpJijgA4zJx2WQfyDBIF+HVCW3/mvkjwHEmYZlo6
         S6pw==
X-Gm-Message-State: ALKqPwdSJiDsYKkLk3FKo/BDG/DNiZBWVddKO9gFYZSpBC47piebzyrv
	w76iXqC3cMFTK0YTjBPfOKmH/R3R
X-Received: by 2002:a81:994e:: with SMTP id q75-v6mr4921607ywg.476.1527606957203;
        Tue, 29 May 2018 08:15:57 -0700 (PDT)
Return-Path: <shu...@sandiego.edu>
Received: from mail-yb0-f171.google.com (mail-yb0-f171.google.com. [209.85.213.171])
        by smtp.gmail.com with ESMTPSA id x125-v6sm14919347ywf.106.2018.05.29.08.15.56
        for <homotopyt...@googlegroups.com>
        (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128);
        Tue, 29 May 2018 08:15:56 -0700 (PDT)
Received: by mail-yb0-f171.google.com with SMTP id w3-v6so2609304ybq.10
        for <homotopyt...@googlegroups.com>; Tue, 29 May 2018 08:15:56 -0700 (PDT)
X-Received: by 2002:a25:2bc1:: with SMTP id r184-v6mr9889524ybr.120.1527606955979;
 Tue, 29 May 2018 08:15:55 -0700 (PDT)
MIME-Version: 1.0
Received: by 2002:a25:d2ce:0:0:0:0:0 with HTTP; Tue, 29 May 2018 08:15:35
 -0700 (PDT)
In-Reply-To: <06B9C5AB-C7CB-4CB5-B951-64E0C4180AD9@exmail.nottingham.ac.uk>
References: <CAOvivQxmrTLRW8wk7cu+A9zF3LCrXSfqsp6R2UN_sz9tF-5UHQ@mail.gmail.com>
 <CAOvivQyY1k+KE9PztsNq6uhZGuV9D3pOYznnbB4p81s4=iHK0g@mail.gmail.com> <06B9C5AB-C7CB-4CB5-B951-64E0C4180AD9@exmail.nottingham.ac.uk>
From: Michael Shulman <shu...@sandiego.edu>
Date: Tue, 29 May 2018 08:15:35 -0700
X-Gmail-Original-Message-ID: <CAOvivQw+-fuPg=8gd=cvTsY++iqH4+=B4QRHQcm8...@mail.gmail.com>
Message-ID: <CAOvivQw+-fuPg=8gd=cvTsY++iqH4+=B4QRHQcm8vK6FwQSkGg@mail.gmail.com>
Subject: Re: [HoTT] Re: Where is the problem with initiality?
To: Thorsten Altenkirch <Thorsten....@nottingham.ac.uk>
Cc: "homotopyt...@googlegroups.com" <homotopyt...@googlegroups.com>
Content-Type: text/plain; charset="UTF-8"

On Tue, May 29, 2018 at 2:15 AM, Thorsten Altenkirch
<Thorsten....@nottingham.ac.uk> wrote:
> What I am arguing about is the way the syntax of type theory should be presented.

I think the answer to a question involving "should" depends on what
the goal is.  Certainly there are situations in which an intrinsic
presentation is valuable.  But because of this:

> we have to eventually connect
>things back to untyped syntax, because untyped syntax is what we write
>on the page, and what we enter into a proof assistant.

I believe there are also situations in which an extrinsic presentation
is essential, and not just a "legacy" way of thinking (at least, not
until someone invents a pencil and paper that include HITs as
primitive).

Mike