From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 2002:a37:7e83:: with SMTP id z125-v6mr4232949qkc.16.1527182815402; Thu, 24 May 2018 10:26:55 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:ac8:3f2b:: with SMTP id c40-v6ls11351332qtk.0.gmail; Thu, 24 May 2018 10:26:54 -0700 (PDT) X-Received: by 2002:ac8:183:: with SMTP id x3-v6mr4297540qtf.32.1527182814656; Thu, 24 May 2018 10:26:54 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1527182814; cv=none; d=google.com; s=arc-20160816; b=ASbRTYI5ufp0vVYFK7G/lPYY0xWXVi2feDWbDnwToHxQDXKE74ZUmX8RopOEGSuJfn gBmgx13IZlhTJ+aA+ogDuff3AnDwiEH4WSudLuHrmn15U5vf6FRH7Smdc4Cnahf81XQp kEFBe6A+kDWJ0jxtgc9PpCb1fpCRVnRmQPnSx437gpUIYWIatTs/KBoVse1b0uDpoiU3 b1RvN337zLDsYCGJtnoGx3Ses171ll368zlImfBwwouuHlmtGFgh1BqnLk7oO/kZmzbz CpoXO6cUHeOcdCiNHdJWubKlLpn+IS1rzXOwTUQ2WfEiSoER8paCr+Vywb2BohAs7Kg9 4/EA== 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=Z68nUwZVP7oTlIDLpaeBrNc6qkKDtSu6c+6Bz9nLixg=; b=qx4+PfeJlyaKZbvOvPV3lA4NbNHlHt4+BkmCgZwM59Dc2md5gYK1viCWhsonWA3Z7L ylS6MafaecsTF8MWfNgHOG/LuBWL6n9fzD1hUXWo0hSeNuvfTmjLo0Kh3vO5+kSWOaq+ 4f2Qq+cgW9nxVHLJZO0FAsvYfvg/9iLjqGa0LY+f41//4dX25+xbnfKGLe3fIz1vGGgS FLdiIitIsGvQUKZo9CaRtI4CVtiB4PoFKg2CVQ2uRDPkRPgykcInvRrmGbyVOX7EvduZ 0a/nOwL19DTwuIcPVIOicEbIFCKs3RKP5QDSz/oB9/QIWJ8NrwCT3RQbzDn/xwFtBefD td4g== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=vxG5CicH; spf=neutral (google.com: 2607:f8b0:4002:c09::22c is neither permitted nor denied by domain of shu...@sandiego.edu) smtp.mailfrom=shu...@sandiego.edu Return-Path: Received: from mail-yb0-x22c.google.com (mail-yb0-x22c.google.com. [2607:f8b0:4002:c09::22c]) by gmr-mx.google.com with ESMTPS id m187-v6si1498948qkd.0.2018.05.24.10.26.54 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 24 May 2018 10:26:54 -0700 (PDT) Received-SPF: neutral (google.com: 2607:f8b0:4002:c09::22c is neither permitted nor denied by domain of shu...@sandiego.edu) client-ip=2607:f8b0:4002:c09::22c; Authentication-Results: gmr-mx.google.com; dkim=pass head...@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=vxG5CicH; spf=neutral (google.com: 2607:f8b0:4002:c09::22c is neither permitted nor denied by domain of shu...@sandiego.edu) smtp.mailfrom=shu...@sandiego.edu Received: by mail-yb0-x22c.google.com with SMTP id i13-v6so876835ybl.4 for ; Thu, 24 May 2018 10:26:54 -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=Z68nUwZVP7oTlIDLpaeBrNc6qkKDtSu6c+6Bz9nLixg=; b=vxG5CicHg6TAY8zCY4tFvFF7o/EBc7bQl5jD0VyCpkrF6QVSYn4JapEI150QXEU+ym yh9kKwgldJj7XfL6Dd6W9L91/Wz9kKBTP3ePKT68exH6MVIGUU+r3n4gtKiyEPTo6sO5 GGRcMLm1cSx1IpzK7pxt2ZEQyWUkhSBTVMokXOKSzu0+VNyk7S0xTkcpxM7aVl4e8act v6hFKHGSRY1Wz12dw4On6yCxoYwH6/3WPTEtQXE2CQDa5npYHhtv25IGxlsbi+lqCZvD zOAn/Uw2cAra3aeXk+PqoFxzYE/sq0VyCo30e2ddfkOA3D86gEsD7ySooYs7y9OpGX5r QLdA== X-Gm-Message-State: ALKqPwcL/7woVJPyxKLdPLu5LDBHc1MnjesrHdvMnVtAi+WfchR8x5h9 2RkF7P7EmdnlAQHJ9pFqsl7fvrew X-Received: by 2002:a25:4555:: with SMTP id s82-v6mr4972849yba.43.1527182814346; Thu, 24 May 2018 10:26:54 -0700 (PDT) Return-Path: Received: from mail-yb0-f171.google.com (mail-yb0-f171.google.com. [209.85.213.171]) by smtp.gmail.com with ESMTPSA id t63-v6sm10355071ywt.56.2018.05.24.10.26.53 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 24 May 2018 10:26:53 -0700 (PDT) Received: by mail-yb0-f171.google.com with SMTP id g140-v6so877845ybf.6 for ; Thu, 24 May 2018 10:26:53 -0700 (PDT) X-Received: by 2002:a25:22d4:: with SMTP id i203-v6mr4662891ybi.505.1527182812869; Thu, 24 May 2018 10:26:52 -0700 (PDT) MIME-Version: 1.0 Received: by 2002:a25:d2ce:0:0:0:0:0 with HTTP; Thu, 24 May 2018 10:26:32 -0700 (PDT) In-Reply-To: References: From: Michael Shulman Date: Thu, 24 May 2018 10:26:32 -0700 X-Gmail-Original-Message-ID: Message-ID: Subject: Re: [HoTT] Where is the problem with initiality? To: Ambrus Kaposi Cc: Altenkirch Thorsten , "HomotopyT...@googlegroups.com" Content-Type: text/plain; charset="UTF-8" On Thu, May 24, 2018 at 2:53 AM, Ambrus Kaposi wrote: > 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 This is the sort of thing I was hoping for. But how far is this from a translation of (5) to (1)? Shouldn't a typing derivation in (5) be essentially a certificate of success for typechecking it?