From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.4.2 (2018-09-13) on inbox.vuxu.org X-Spam-Level: X-Spam-Status: No, score=-1.2 required=5.0 tests=DKIM_SIGNED,DKIM_VALID, DKIM_VALID_AU,DKIM_VALID_EF,FREEMAIL_FORGED_FROMDOMAIN,FREEMAIL_FROM, HEADER_FROM_DIFFERENT_DOMAINS,HTML_MESSAGE,MAILING_LIST_MULTI, RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.2 Received: from mail-it1-x139.google.com (mail-it1-x139.google.com [IPv6:2607:f8b0:4864:20::139]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 6d223cac for ; Thu, 3 Jan 2019 15:00:14 +0000 (UTC) Received: by mail-it1-x139.google.com with SMTP id o205sf35854692itc.2 for ; Thu, 03 Jan 2019 07:00:13 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1546527612; cv=pass; d=google.com; s=arc-20160816; b=lK3iOAxRuSKqUMlfE/QK8XycSYiJYEe1FMPc9H/IbtIQ+MOdWygkcIuiegyl8Huges rPfx34FK8LfBrwf0dmUBHpT0KIVJ8exqtYVlew/VCceps1Imy1a37FcALl/eKBd7a1MA EAgMa7X7Wrj87R88QpFcbvKTsLr9wXhre+s20ysh9wdO/NY9KvD7qWhpzb2o4T6sMV/0 pZuSGP/IAJCzPJWp89eMa4o61st8qWMUlTSk7esFmjbUt80uWCx5GBCesjsQ83Jp+FcI yL+Tq6xwZGdNNdJ5BJpYBafbeotNp6fsmJYgMUJ89BhyK4y/Rhr22hFIMt/eXkJMZhPG DNGw== ARC-Message-Signature: i=2; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=list-unsubscribe:list-archive:list-help:list-post:list-id :mailing-list:precedence:to:subject:message-id:date:from :mime-version:sender:dkim-signature:dkim-signature; bh=JleND7nElbUKxf1ARMiYxSEa8etvit6J5H0r/3ETz9k=; b=FfPdn1yxISeXeWjIX3iZ9mpHaMibRtl37uOhCQcjNUaVc4eBUn+N3s53zhm4d+SCu6 zHNHcarbfLXKR5qE5lO1Sz7FIjbi2e4bSj69+EpI95RrXHsu6agbxKyH1vVAuL81eO8V 4ix4mQen4/IjyhwzmS/EQofTjtifGr7nNv8rF/TwtThJqutD5OGyYs7YQ1u4aqVSIULs Ut3NQSYzjwlXRgpyq+qYBJfyk39AFBaDWXCLH84aGW881kbuMr++xQD964xiGQw62IIp YC8F211fevv1EMdl/RljU+o5nOefnf7Tnma9mmPCtoLMeXfV0ZMHmlV5Kd3WBAZ/dO41 gVMg== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=aj36qfqF; spf=pass (google.com: domain of evancavallo@gmail.com designates 2607:f8b0:4864:20::22b as permitted sender) smtp.mailfrom=evancavallo@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:mime-version:from:date:message-id:subject:to :x-original-sender:x-original-authentication-results:precedence :mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=JleND7nElbUKxf1ARMiYxSEa8etvit6J5H0r/3ETz9k=; b=lbU/egZm1UfJ0vGgtUeZ4FBqxIRpdubjI5tqib5QVSo9dBmLrSa1j5e3wbpfWV7kVs bk4k8TTsg6pUCgXz631mVVfjpT/nDJKo6zufyfBKiW+GBDyK+QWMrbpMjrQRn3Rh3NKT nq6etwyOYAuGPaqEahT33nTC4OMaU8JN6zVtxc+r0f+x69FcLq1kgGqnYBKPRUv6hg3N a5TQstv3GKZU5Xt5i2c4pfMCbxENwPjOvOQ+AxIDcgCUxg+wT9uDChYGFNDUbMGJTlXO sOPRh1nIhWf+ynBTlwk6xqS45bCqRN7LwSym2v6ijMpC+uD5Idd0lpd+nXhypAMtnb2Q zlgg== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version:from:date:message-id:subject:to:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=JleND7nElbUKxf1ARMiYxSEa8etvit6J5H0r/3ETz9k=; b=usFHuyN52EIgEZo+PC78SyVo5v8poKHduilN9ExTZApwOu0tqbwqH7GtHef0S6y9m8 IpRBYKdYFTOYKKMxG+IO9TGSpt0gDi7mqT1sK4U3Lwvm696+m77A0nww8PniJGg8Nap7 +aT9c3SZK4ZK7a0o7xTcSU1QS2c58CJ4E3QbTWuxTUZaUiLNhZNabTJx3G1kpuCKPj/g 0aHGd2Vj+qu9J+6+qx6/RKySPsGwXwyBe8cUbhluXobFhuN2w33n5pSs9vYLptTBPZqC DtylrSGfzQ0fQLkQp05DLwC0JiogtzxeWDEtgMl/xmddoiqvhPz7TJqjYphaBdb7G2EM +2Ew== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:mime-version:from:date:message-id:subject :to:x-original-sender:x-original-authentication-results:precedence :mailing-list:list-id:x-spam-checked-in-group:list-post:list-help :list-archive:list-unsubscribe; bh=JleND7nElbUKxf1ARMiYxSEa8etvit6J5H0r/3ETz9k=; b=AD9eItCed7M4wxFhquHSlU2ZHul7W7n0YSS++qSYE2AvfX8sdt+4XTQNRjJRcmT4Zi xMHMDQHrEtUEqo8fInbgtXMq+DybTu2mL/vUMSD8VCiFHqNs58h+eAxTBeCj65hUm/Tj jHLBGNwvjX9EfBdRTTebKQYvm7+E65odypG9aXZ1oMbHF/1BEAwxRzglqd0I/TVkzf2L CnkesZRlodSMHcYy0Z0NzFPRryzyvqkPZObm0qr3fpZ6kIx/POjfyyicQtkVsOBdToY8 phNQdZZfc02JaLtwGwJYN7lnn6CzXB5PA00cnki0387iqsbKO1kCd1yM0Ig5Sa2cytXT 7Hkg== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AJcUukcIy/xi4VBJhz/y8hHmmGbgE+Ns3vao/2JmXOnlNiQkj/zMaOiX 8Kr6l1w/9EE0oHYIWM116Xs= X-Google-Smtp-Source: ALg8bN4YavSzGQ+Yknh2FGQSXcYpN12ngK2gywX/MPdMHVBMiNTt66yED5i2Y7e3gfC5a9rR+PvV2Q== X-Received: by 2002:a5d:8b85:: with SMTP id p5mr82395iol.7.1546527612477; Thu, 03 Jan 2019 07:00:12 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a6b:3c12:: with SMTP id k18ls12455549iob.2.gmail; Thu, 03 Jan 2019 07:00:12 -0800 (PST) X-Received: by 2002:a6b:680a:: with SMTP id d10mr28078857ioc.35.1546527612215; Thu, 03 Jan 2019 07:00:12 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1546527612; cv=none; d=google.com; s=arc-20160816; b=s8Giz4cTsA1HdvIOVBh2rFeA44xFHq7MvLocv61O5lfz8l6Fy947soUt0xj6m62Oe8 4uay1t755iH/htDLwCesb2JdDJ++6IXtF/wNTY101BzIqUNfL1LMKQJyRkLjKu6mam4L p+tuNqvdsPoofkdByxqDGGuDHX2zWUXkCoIvQITnbS/UGA4qSD5EZJ+8AlMwv3uhlik0 RLlJ5q4/RjjLF0lgdadLzwZbh3d34UA1Jp/+Iq39v5qVmyVfgnbq4PHbiiX0IGh9VcKD aMVbDVJnlykB7hwqiE5gvvFce82qW8nrZN5l6ap15quACs9/cpQhuUAsFJ9VQOto81Ih LrUQ== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=to:subject:message-id:date:from:mime-version:dkim-signature; bh=2rWwBpA81HWABNcOSFgSkA33o0coTxtrZkQDh3ZqYo8=; b=iKmoThTei/YQpA6WwU0iuKrVDU52FlacrvTAPHvIZ3Zg0vTg8WHFFgcddMxmg9wqAe dkqnMtAz3nNyQ8FzLiwuoB5y9i0DIr6wNeaRrU5T/V1j0KJlQMYEi5tT5PUrLa6/Km3h ML/o+aQCwqO7Z9LoDErLvAfhdN3ynOxuqQXz38hLHrBxmUbGhTuCj8xcDCV7Nx4M6oXg SRsY4NtSIRFTK4jGp4dnn9gZTlVQDy2fXWl3T+oLOOOR21boVZRBMFt7ddjRCq/AV+nd wg7ySDzgZv8m446s1bn0jQ3lTCOrWEeIGdMgIfkG49df9v8bCe1j3s9O10+caAGMrWPs fnIQ== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=aj36qfqF; spf=pass (google.com: domain of evancavallo@gmail.com designates 2607:f8b0:4864:20::22b as permitted sender) smtp.mailfrom=evancavallo@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-oi1-x22b.google.com (mail-oi1-x22b.google.com. [2607:f8b0:4864:20::22b]) by gmr-mx.google.com with ESMTPS id x9si3174953ita.0.2019.01.03.07.00.12 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 03 Jan 2019 07:00:12 -0800 (PST) Received-SPF: pass (google.com: domain of evancavallo@gmail.com designates 2607:f8b0:4864:20::22b as permitted sender) client-ip=2607:f8b0:4864:20::22b; Received: by mail-oi1-x22b.google.com with SMTP id y1so27869835oie.12 for ; Thu, 03 Jan 2019 07:00:12 -0800 (PST) X-Received: by 2002:aca:54c4:: with SMTP id i187mr31002437oib.238.1546527611530; Thu, 03 Jan 2019 07:00:11 -0800 (PST) MIME-Version: 1.0 From: Evan Cavallo Date: Thu, 3 Jan 2019 10:00:00 -0500 Message-ID: Subject: [HoTT] Parametric cubical type theory To: Homotopy Type Theory Content-Type: multipart/alternative; boundary="000000000000ebb15b057e8f047b" X-Original-Sender: evancavallo@gmail.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=aj36qfqF; spf=pass (google.com: domain of evancavallo@gmail.com designates 2607:f8b0:4864:20::22b as permitted sender) smtp.mailfrom=evancavallo@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Precedence: list Mailing-list: list HomotopyTypeTheory@googlegroups.com; contact HomotopyTypeTheory+owners@googlegroups.com List-ID: X-Google-Group-Id: 1041266174716 List-Post: , List-Help: , List-Archive: , --000000000000ebb15b057e8f047b Content-Type: text/plain; charset="UTF-8" Hello all, We have a new preprint out on the arXiv, about combining cubical type theory with Bernardy et al.'s work on internalizing parametricity. "Parametric Cubical Type Theory" https://arxiv.org/abs/1901.00489 Best, Evan, w/ Bob Harper -- 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 HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout. --000000000000ebb15b057e8f047b Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Hello all,

We have a new preprint out on the arXiv, about combining c= ubical type theory with Bernardy et al.'s work on internalizing paramet= ricity.

"Parametric Cubical Type Theory"=

Best,
Evan= , w/ Bob Harper

--
You received this message because you are subscribed to the Google Groups &= quot;Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an e= mail to = HomotopyTypeTheory+unsubscribe@googlegroups.com.
For more options, visit http= s://groups.google.com/d/optout.
--000000000000ebb15b057e8f047b--