From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 2002:a63:330c:: with SMTP id z12-v6mr1153542pgz.91.1527155612158; Thu, 24 May 2018 02:53:32 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a65:4345:: with SMTP id k5-v6ls4720262pgq.4.gmail; Thu, 24 May 2018 02:53:31 -0700 (PDT) X-Received: by 2002:a63:721a:: with SMTP id n26-v6mr1170864pgc.107.1527155611168; Thu, 24 May 2018 02:53:31 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1527155611; cv=none; d=google.com; s=arc-20160816; b=vBFHqk0k7DZwpw6AEXLfTN2FH1SsAZx+648fp6YztXpY/WUXgBRyL1EqpYCkbG2CqD Up3m5b5fXl777yKVGaEq+TaN4yNCMGd9VIQb9QXmVQjUGKQ4tnwqwvITVkL1toR77YLP i+dZCiImZcJTuT9qz5SSbfPAnGdTFd+3umYyyR1ZO3TZyCavFmqTGrv7rf/erbr9CWz3 R4lds3Mfaw7n6uncINq7e0KCy1dHv4HN9zW1800tnl6D/ueIZXfVPY3UG8zA71e7xqmd NQLuBeqyY3PvcPHzUgm1BPw+vGEI85U5gbEsBcOIr6LSqvcEurfJwdO3ozMAxM/DGg7I 4SUw== 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:arc-authentication-results; bh=swlGxk3+1zgB7rz154T1UP0due5myk705z4K7D3QHQI=; b=XbO09n6k7+yorITzso1Wp37011XqwDdYIxXL2lI1DMf2nHRfbNG26dhBBWwKWhZWwV WXT+hfQe5LJmbUdxqztHfxOkQh0dQU5xOkMZu73qKQWSyuLDNxO9MLTr99obiaZ2dmnj FFLaEnLzaivU9sdrrFdc0M2Z/ofAtkPglsZzk7rI+43H4B5fE7gp2oiWliFiDXRdC+SK BF89gOic7/zhIKWM9T2910+j37uwqY6bkknNosG5Iw136+sMmNfUbT7/vX/NR7EYorCX Th+L/46wuD4VtABqOaj9j5SOplc5CvGpmsz5ZD2c3iQ+rc0qAgucTvX0n3P36Vjw6DHw ROsQ== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=sf/n0PLr; spf=pass (google.com: domain of kaposi...@gmail.com designates 2607:f8b0:4001:c0b::234 as permitted sender) smtp.mailfrom=kaposi...@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Return-Path: Received: from mail-it0-x234.google.com (mail-it0-x234.google.com. [2607:f8b0:4001:c0b::234]) by gmr-mx.google.com with ESMTPS id n10-v6si1742511plp.2.2018.05.24.02.53.31 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 24 May 2018 02:53:31 -0700 (PDT) Received-SPF: pass (google.com: domain of kaposi...@gmail.com designates 2607:f8b0:4001:c0b::234 as permitted sender) client-ip=2607:f8b0:4001:c0b::234; Authentication-Results: gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=sf/n0PLr; spf=pass (google.com: domain of kaposi...@gmail.com designates 2607:f8b0:4001:c0b::234 as permitted sender) smtp.mailfrom=kaposi...@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: by mail-it0-x234.google.com with SMTP id p3-v6so1591047itc.0 for ; Thu, 24 May 2018 02:53:31 -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=swlGxk3+1zgB7rz154T1UP0due5myk705z4K7D3QHQI=; b=sf/n0PLrcugUdEAMU1QbjPSDFVqZhLYm1cJp4K6vgWuFS0COyPbRcKU1UuWjex0/R0 AsFC9q3kISI5LRgT7DppxpX1NN9edfMIvZW9RSiACZ0XxhxyUpp52ifTfge2YF4q8EBb 3qipLo55mT3iOHi/fz5Msm0d7JeRkjRxap3VrYNGGlV6p56QBoWWk0aZyp89kvrC7C6h N6fRHbr5OpnsE/NgRyN2LyjmafFwJnJ+0Aam/0OqfMhWRsVowfh+WQMn1iOmnVpfOKhL zK8d489dxQE5eV6mz4Rw6cl4Ii3QyYVOiNaWNtvSX6ocD852zUykYKW/p2o/3WIc/xZm Wlrg== X-Gm-Message-State: ALKqPweo285CCNqLUVkwZ6JTL8pxwVti7E7+8VTXGRNDN+7zRXc0ICga f8reEeOu7Q9xuAFqYedu7BbhxclsaPNvgHX2ccA= X-Received: by 2002:a24:97cf:: with SMTP id k198-v6mr4504482ite.105.1527155610925; Thu, 24 May 2018 02:53:30 -0700 (PDT) MIME-Version: 1.0 References: In-Reply-To: From: Ambrus Kaposi Date: Thu, 24 May 2018 11:53:17 +0200 Message-ID: Subject: Re: [HoTT] Where is the problem with initiality? To: Altenkirch Thorsten Cc: shu...@sandiego.edu, homotopyt...@googlegroups.com Content-Type: text/plain; charset="UTF-8" On Thu, May 24, 2018 at 10:11 AM Thorsten Altenkirch < Thorsten....@nottingham.ac.uk> wrote: > >>(5) and (7) introduce preterms which I think shouldn't be considered > >> fundamental in the definition of type theory. > > > >I have to disagree here. In my view, 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. (We don't need > >to go all the way back to character strings -- parsing and lexing are > >essentially solved problems in any language -- but we do need to get > >back to some kind of untyped *abstract* syntax such as in (5).) The > >various kinds of typed syntax are useful and important intermediate > >objects, but at some point there has to be a step that formally > >explains how to produce "typed syntax" from untyped syntax. > Indeed but also type checking and scoping are solved problems. Just to clarify this: you don't need to go through preterms and typing relations to do type checking. You can write an algorithm which takes untyped terms (without explicit substitutions) and returns intrinsic (well-typed) terms. It only needs conversion checking for intrinsic terms which is also a solved problem. Here is an example implementation: https://bitbucket.org/akaposi/tt-in-tt/src/HEAD/Typecheck.agda