From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 2002:a19:d042:: with SMTP id h63-v6mr586222lfg.19.1527916880359; Fri, 01 Jun 2018 22:21:20 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a19:434d:: with SMTP id m13-v6ls4587679lfj.13.gmail; Fri, 01 Jun 2018 22:21:19 -0700 (PDT) X-Received: by 2002:a19:1a51:: with SMTP id a78-v6mr588292lfa.17.1527916879193; Fri, 01 Jun 2018 22:21:19 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1527916879; cv=none; d=google.com; s=arc-20160816; b=HHe2zr2oByHSDGzCGYzBOyO0W8M8+u+INYP06s0dfkQZhnUKedVyQIN/gfZ9lZt3aY nz88PEfgXraEsbDYA9uZlKtVxsQkS4yZ3vOSauuGFPHiYqF1KS+bEkOqQfq8v+1fEybN YXGKUfH/I/oW5M+JEgwFCCGASjT7ohNzJXFl/qclJYWDKSUK65DXqXW5cJnPNs9VZqfz 3Ni32pKaGOGvfIc23kgAtVQKR/dTIhaWHd47XV4REELoxVLLAjZGrSogLCRF56kKFO40 EExn+7+6S0nXl7wdwxMLyIEeG3ROGggvvcU1uKFrHfECNaQ0M4f9C1VJwZb3BpKOs0X0 Sq5Q== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=content-transfer-encoding:cc:to:subject:message-id:date:from :in-reply-to:references:mime-version:dkim-signature :arc-authentication-results; bh=V/933/eOxXnadZTdtVDK6Hc4GN7Bu/V1oHv7Laf4gHg=; b=cHHeA3yUgv7OSo4/DjRLMwyVEA8PRWQ1TndpfQm1vo+S2cG3RXThxzzF4b3rLXpEh1 uRFi8oe0v15EE9KJ4Pt6Xaeb3vrU12thcpv9ZCQw+dgvMTzBA0V5J2HUwvpuMH9N8xpS 9Eif0Unwqj+lpbC8HckMbR6EOmtS3nlmOS0FvQnyc57kFASG+Mitm+gO9IG6m4nWifNC QL5XkezVGhtycbcKjnEKkcePXM4aou7bPituEO3z4kgFR3r9/xKYKgOtgVDhkfpXBuN1 7LM8AZtxATXE8C3hixavd6QkS+0WJLXs89bPPeZ6TVx9IVxAk5rTQSajQiIpXf9j5+3j Opcg== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=E3ZNq8BD; spf=pass (google.com: domain of kaposi...@gmail.com designates 2a00:1450:400c:c09::22f 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-wm0-x22f.google.com (mail-wm0-x22f.google.com. [2a00:1450:400c:c09::22f]) by gmr-mx.google.com with ESMTPS id l24-v6si40243lja.1.2018.06.01.22.21.19 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Fri, 01 Jun 2018 22:21:19 -0700 (PDT) Received-SPF: pass (google.com: domain of kaposi...@gmail.com designates 2a00:1450:400c:c09::22f as permitted sender) client-ip=2a00:1450:400c:c09::22f; Authentication-Results: gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=E3ZNq8BD; spf=pass (google.com: domain of kaposi...@gmail.com designates 2a00:1450:400c:c09::22f as permitted sender) smtp.mailfrom=kaposi...@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: by mail-wm0-x22f.google.com with SMTP id l1-v6so5703030wmb.2 for ; Fri, 01 Jun 2018 22:21:19 -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:content-transfer-encoding; bh=V/933/eOxXnadZTdtVDK6Hc4GN7Bu/V1oHv7Laf4gHg=; b=E3ZNq8BDnRk8ddQU9jFhgEqlhpSeSERjs1hZ9uhZF/ljhJlz7X4CoQYYbJP/Kv2R+s 2+pS2S/eouix8LZ0W1MQ+k1WzMunnrXRzA9vGS3Tav9hxGDdJOVYvwFxbO6Bf7tJ5d51 XiljrIiRlItztxSmiil04hfan24C/mlKpj4xDUZB8kP3m6gX/oHOyxjQm9qV7t0glOey 4fBb8XNZy5obwtIFXkKL237uBvewxnGCetqJ3YVvE1xR4r9JdJGrKNKiHzc9bJooIkjS cVgaeSbvWyGgSqY2GFPOJiUC99J40AvSvID52Dk3a+Yy80cJ0yp2jOrFqfaZ0+Qalrv3 ztLw== X-Gm-Message-State: ALKqPwcItG+c3sAXc1R6isbhyhxaIEdRQnQigsvAH2DJQpfBnB2ImbPI IkONzlx2BDSLJKjtE9FHpgg/stnQiPHG7jhcuog= X-Received: by 2002:a1c:9d49:: with SMTP id g70-v6mr4584947wme.134.1527916878842; Fri, 01 Jun 2018 22:21:18 -0700 (PDT) MIME-Version: 1.0 References: <06B9C5AB-C7CB-4CB5-B951-64E0C4180AD9@exmail.nottingham.ac.uk> <20180530093331.GA28365@mathematik.tu-darmstadt.de> <5559377C-94C9-422E-BBF7-A07AFA4B7D04@exmail.nottingham.ac.uk> <3D1D292E-1EFF-4EA2-8233-B55FDA5CE8A5@gmail.com> <5A8268CE-26C1-4FD5-A82F-8063C08EF115@exmail.nottingham.ac.uk> <37CBB960-C4F1-4B97-92E6-28462A0591C1@gmail.com> <2b190a31-7985-4e6b-9f69-ed244ea64d7d@googlegroups.com> <864df164-59e9-4609-8e81-7c334be11e98@googlegroups.com> In-Reply-To: <864df164-59e9-4609-8e81-7c334be11e98@googlegroups.com> From: Ambrus Kaposi Date: Sat, 2 Jun 2018 07:21:06 +0200 Message-ID: Subject: Re: [HoTT] Re: Where is the problem with initiality? To: atm...@gmail.com Cc: HomotopyT...@googlegroups.com Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable On Fri, Jun 1, 2018 at 11:27 PM Matt Oliveri wrote: > > On Friday, June 1, 2018 at 1:45:42 PM UTC-4, Eric Finster wrote: >> >> So from an internal perspective, I cannot think of any reason to >> insist on decidability. > > I agree with this. And in particular, I think QIITs can define intrinsic = syntax of (fully-annotated) extensional type theroy just fine. Equality ref= lection would be an extra equality constructor. Isn't that right? What do T= horsten and team think of that? Is it an infelicity of QIITs, perhaps becau= se they're hSet truncated? Or is there a problem with ETT that structuralis= m doesn't shed light on? Or is ETT maybe not so bad? Yes, the syntax for extensional type theory can be defined as a QIIT. For me, the problem with it is that there is no easy way to input terms in the computer: starting with a string, lexing, parsing it and getting an untyped term, then typechecking the untyped term. During bidirectional typechecking, we need that types in the QIIT have decidable equality. See e.g. https://bitbucket.org/akaposi/tt-in-tt/src/HEAD/Typecheck.agda Equality of types is not decidable in ETT, even if we can normalise terms (use it for programming). But maybe there are other ways to build terms in this QIIT in a convenient way (the NuPRL, Andromeda people know this), and then I also don't see why we would insist on decidability of equality.