From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.107.199.198 with SMTP id x189mr13636452iof.81.1501604810189; Tue, 01 Aug 2017 09:26:50 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.36.34.199 with SMTP id o190ls1440221ito.21.gmail; Tue, 01 Aug 2017 09:26:47 -0700 (PDT) X-Received: by 10.159.59.222 with SMTP id y30mr14020206uah.38.1501604807604; Tue, 01 Aug 2017 09:26:47 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1501604807; cv=none; d=google.com; s=arc-20160816; b=ETiFI9zvVWFZ6cD4p0RHhwd3wfMlAHPJXfsvNPwN86gVyx22AJOu7IKg0PeyGQev4s 45XWIgtKkKNTId/Ope8b6D3XSHAME68NFR+mMPEqGE+GxNQf0tOSqA1H+rtihn4e6TMC cGESOlYujK/BiSw0L5uq331UO52PbYBujIPg9tBAiDLORSIXXaO9Dm+tHpOiq2RnwINd T5R3vrLHCu8NkysKZfDO5ldg269oFdStIl3sjGqT5DB69Tl9T0rDqUnHL+s1ZO8YDhhw rBe3fClmkcLZRqBdDeG9EOIQwf7twYYSBlTwDvlbulSxiwFiQMxABWxwEyI6dL3cVkG4 1rQQ== 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 :references:in-reply-to:mime-version:dkim-signature :arc-authentication-results; bh=5sFYND6zQa18rYANv4qLcs+Ku/0v9c7OS2gG4+mIyDI=; b=EImNFo4c7HuyYDweNicjJVdDwlW49/ZTFlwo/MciJg2ozIrHR58nupDXijcIj0stk1 hJreS/p6hB0x7irrNzpfwgDqkAUztBA9eM49O2VtVbAfk/RZOuacWFQBFPhPkCnpcgkh +v5volseOwhrPfSt01mR6sSjefONvZR3Ceo6nwyPjODwyha3H+V/gvj4nPZgZYSiWgGy B6WDmwxKE7yAo+LQRhkr0AJrWWTLCGy55S0s9l93MOOWq8uHVnKXJVCBAsSZOWVbrekH 30pLNQOOdSLl9j8B0+Y13uYwddoo/QndXcDfnabXOFENfC8JWgOyvzMkTKMgTPwTUDeL nOEw== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@sandiego-edu.20150623.gappssmtp.com header.b=TAtw27bv; spf=neutral (google.com: 2607:f8b0:4002:c05::231 is neither permitted nor denied by domain of shu...@sandiego.edu) smtp.mailfrom=shu...@sandiego.edu Return-Path: Received: from mail-yw0-x231.google.com (mail-yw0-x231.google.com. [2607:f8b0:4002:c05::231]) by gmr-mx.google.com with ESMTPS id a2si1788386ywf.16.2017.08.01.09.26.47 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Tue, 01 Aug 2017 09:26:47 -0700 (PDT) Received-SPF: neutral (google.com: 2607:f8b0:4002:c05::231 is neither permitted nor denied by domain of shu...@sandiego.edu) client-ip=2607:f8b0:4002:c05::231; Authentication-Results: gmr-mx.google.com; dkim=pass head...@sandiego-edu.20150623.gappssmtp.com header.b=TAtw27bv; spf=neutral (google.com: 2607:f8b0:4002:c05::231 is neither permitted nor denied by domain of shu...@sandiego.edu) smtp.mailfrom=shu...@sandiego.edu Received: by mail-yw0-x231.google.com with SMTP id u207so13193588ywc.3 for ; Tue, 01 Aug 2017 09:26:47 -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:content-transfer-encoding; bh=5sFYND6zQa18rYANv4qLcs+Ku/0v9c7OS2gG4+mIyDI=; b=TAtw27bviUfBXm4jnfG6Xgh9nkMfz7moYX4V+kORrd3N/aTJdlRppcnrmxLxldRRZw o/ubutDJ0PqYh1WcU8jC1AHupbnOChu0OTT8Xi6OI3GbyAfJbBBIAYTVepcxgnIAPi8T dnA3w8CuB1vAuhJvrnKfpx52QMbWRMHGqgKRafA3Np0bBNuY0Flwto4tH4o5avneRLTU Rfs6KpDng3InWyQBDTxFxO3C5mSLY+idMLdU2xOzNKV0ZQHEDt/fzCK0ZGKDAHNLNj9o n4jvcPH+T/fQBDFEm+es7GhUhWwNQPrurGG7873MCIap00gwFzl0NikMR+PvsZhvDqpt JI6g== X-Gm-Message-State: AIVw110j4JvaPyqd6fEzkLp6SUPVl/IqYnSqYk3dRQ6vae5CZg5poEFd dMvhQa5/XEy1s8ELats= X-Received: by 10.129.175.74 with SMTP id x10mr20043381ywj.319.1501604805499; Tue, 01 Aug 2017 09:26:45 -0700 (PDT) Return-Path: Received: from mail-yw0-f174.google.com (mail-yw0-f174.google.com. [209.85.161.174]) by smtp.gmail.com with ESMTPSA id x203sm6865086ywd.32.2017.08.01.09.26.45 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Tue, 01 Aug 2017 09:26:45 -0700 (PDT) Received: by mail-yw0-f174.google.com with SMTP id p68so13345276ywg.0 for ; Tue, 01 Aug 2017 09:26:45 -0700 (PDT) X-Received: by 10.37.216.193 with SMTP id p184mr6650543ybg.35.1501604804603; Tue, 01 Aug 2017 09:26:44 -0700 (PDT) MIME-Version: 1.0 Received: by 10.37.255.10 with HTTP; Tue, 1 Aug 2017 09:26:24 -0700 (PDT) In-Reply-To: References: <55685b9e-8177-42f0-9cfc-69901115181f@googlegroups.com> <1187de24-0548-48cd-9b7b-c3c3ab9cf4a7@googlegroups.com> <8f052071-09e0-74db-13dc-7f76bc71e374@cs.bham.ac.uk> <38162a12-c8b2-401d-b272-07d1db7c1be8@googlegroups.com> From: Michael Shulman Date: Tue, 1 Aug 2017 09:26:24 -0700 X-Gmail-Original-Message-ID: Message-ID: Subject: Re: [HoTT] Re: cubical type theory with UIP To: James Cheney Cc: Neelakantan Krishnaswami , Homotopy Type Theory Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable I think I've seen something like that too; it seems to be basically giving up on eliminating cuts involving equalities by building them into the primitive rules. I would expect equality to be one of the *logical* operations, so that we can eliminate its cuts, rather than being described by axioms as if it were part of the "theory". On Tue, Aug 1, 2017 at 2:34 AM, James Cheney wrote: > Not sure if it's what you're looking for or if it is an example of a "not > fully satisfactory" system, but Negri and von Plato's book "Structural Pr= oof > Theory" (esp. ch. 6) talks about axiomatic extensions to sequent calculi > that preserve cut elimination. The main idea is to turn axioms of the fo= rm > > P1 & ... & Pn =3D> Q1 | ... | Qm > > into right-rules of the form > > Q1,Gamma =3D> Delta, ... Qm, Gamma =3D> Delta > --------------------------------------------------------------- > P1,...,Pn, Gamma =3D> Delta > > so that no new principal cuts are introduced. This can handle equality o= r > other FOL axioms of the form forall X. /\_i Pi =3D=3D> \/_i Q_i where P_i= and > Q_i are atomic. > > --James > > > On Tue, Aug 1, 2017 at 10:20 AM, Michael Shulman > wrote: >> >> Yes, I think I've seen something like this before. It may give a good >> programming language, but from a semantic category-theoretic >> perspective I don't think it's any good. Two syntactically distinct >> terms might still turn out to be semantically equal, so you need a >> left rule for equality that does more than just syntactically analyze >> the terms being equated. >> >> On Tue, Aug 1, 2017 at 2:14 AM, Neelakantan Krishnaswami >> wrote: >> > On Monday, July 31, 2017 at 4:51:18 PM UTC+1, Michael Shulman wrote: >> >> >> >> Another motivation is that as far as I know, there is not a really >> >> satisfactory version of sequent calculus for first-order logic with >> >> equality (e.g. not having a fully satisfactory cut-elimination >> >> theorem). If cubical methods are a good way to treat equality >> >> "computationally", I wonder whether a "cubical sequent calculus" woul= d >> >> be able to deal with equality better. >> > >> > >> > Actually, there *are* good versions of sequent calculus with >> > equality. Jean-Yves Girard and Peter Schroeder-Heister have both given >> > the appropriate rules. So, given a language of terms with some >> > equational theory, the right and left rules are: >> > >> > >> > =E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2= =80=94=E2=80=94=E2=80=94 =3DR >> > =CE=93 =E2=8A=A2 t =3D t >> > >> > >> > =E2=88=80=CE=B8 =E2=88=88 csu(s,t). =CE=B8(=CE=93) =E2=8A=A2 =CE= =98(C) >> > =E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2= =80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80= =94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94= =E2=80=94=E2=80=94 =3DL >> > =CE=93, s =3D t =E2=8A=A2 C >> > >> > The premise of the left rule quantifies over a *complete set of >> > unifiers* for s and t. For terms freely generated by some signature, >> > there is a single most general unifier (if one exists), and so the >> > left rule has at most one premise. Once you add equations then >> > there can be more than one most general unifier -- possibly even >> > infinite (eg, if terms are lambda-terms modulo beta/eta, as in >> > higher-order unification). >> > >> > The Girard/Schroeder-Heister equality is not the same as the Martin-Lo= f >> > identity type, but it gives rise to a nicer programming language than >> > raw J >> > does, since the left rule is invertible. Invertible left rules are wha= t >> > give >> > rise to >> > pattern matching syntax, and so languages like Agda choose a fragment >> > where the G/SH rule and J coincide to implement pattern matching. >> > >> > Agda restricts pattern matching so that an identity type >> > argument can only have a refl pattern when the two terms being equated >> > are generated from variables and constructors. So an identity proof >> > p : (cons x y) =3D (cons a b)) can be matched as refl, but an identity >> > proof q : (append x y) =3D (append a b)) can't be. >> > >> > This restriction ensures that first-order unification suffices for the >> > G/SH elim, and therefore to implement pattern matching. >> > >> > If you are very interested in this topic, Joshua Dunfield and I have a >> > draft >> > paper where we work out the Curry-Howard story for pattern matching >> > with the G/SH equality (what are called GADTs by PL theorists) in gory >> > detail: >> > >> > Sound and Complete Bidirectional Typechecking for Higher-Rank >> > Polymorphism >> > and Indexed Types >> > >> > >> > -- >> > Neel Krishnaswami >> > nk...@cl.cam.ac.uk >> > >> > -- >> > You received this message because you are subscribed to the Google >> > Groups >> > "Homotopy Type Theory" group. >> > To unsubscribe from this group and stop receiving emails from it, send >> > an >> > email to HomotopyTypeThe...@googlegroups.com. >> > For more options, visit https://groups.google.com/d/optout. >> >> -- >> You received this message because you are subscribed to the Google Group= s >> "Homotopy Type Theory" group. >> To unsubscribe from this group and stop receiving emails from it, send a= n >> email to HomotopyTypeThe...@googlegroups.com. >> For more options, visit https://groups.google.com/d/optout. > >