From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: homotopytypetheory+bncBDDNRA4JSMHRB566SDNQKGQE3USOMVQ@googlegroups.com X-Spam-Checker-Version: SpamAssassin 3.4.1 (2015-04-28) on inbox.vuxu.org X-Spam-Level: X-Spam-Status: No, score=-0.6 required=5.0 tests=DKIM_SIGNED,DKIM_VALID, DKIM_VALID_AU,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.1 Received: from mail-oi0-x23c.google.com (mail-oi0-x23c.google.com [IPv6:2607:f8b0:4003:c06::23c]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id ae9e6546 for ; Fri, 3 Aug 2018 10:33:29 +0000 (UTC) Received: by mail-oi0-x23c.google.com with SMTP id s200-v6sf4351037oie.6 for ; Fri, 03 Aug 2018 03:33:29 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:date:from:to:message-id:subject:mime-version :x-original-sender:precedence:mailing-list:list-id:list-post :list-help:list-archive:list-unsubscribe; bh=2PUD1wjT144JYKET2oTTOKDbOJS0iTP3wQvRACKFgpE=; b=b25GRSQBYQzGsPTNxn22QnhZQJSej+lBx0K3QqMNo/SeY6aJAfOjw4DM0GnKaND8BP 7bKF4kmTyWst+KLkX94y1paDDORDTEh4Q6/wpmh+tPKs9BdZz6n3PZQXyKh9jWLG7cpk 5aK2G+wFvQtoM1d1ckTCg6dUhOnpDiF+TyavT2YvBLq9MPlWKkAU8BCQP/NUNaGTVny3 Zs9h+dkDcmp1IetRawyfNoQcNBB5HEG4ERg6Ft1fWQTOk0q8e4UXdipzSyR+3ORpKSvj AXB/+ovfSEgFmiIzxmbBEoehyOOe0CsSkSUMBX2t+Wk+HTRC1eyeKOXQQ/OrgX1YU5XA /Cag== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=date:from:to:message-id:subject:mime-version:x-original-sender :precedence:mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=2PUD1wjT144JYKET2oTTOKDbOJS0iTP3wQvRACKFgpE=; b=nHBtDiZy+aV4hS5FjemQtXTTtVzkRuuSA47KyWrnVGTOgtVfuDie/OEp9SIqO6Gqx+ l+jWsMbfAPI5npoqJedqWuEFcuHEXLF34j667styDEVz1QPmvDIG3ObpoS7ejp9HMP10 V4/fLsctLUvjz2OIRigSYUlXV39i0/Z1Ps9s9uO4knjIndcsY3RTrfeGrcKUFHFuqYWQ dEvobdOzISW5OZk9QePsUExooeyq6LUe7CIedFhyFlP562P4CtFFFRr1MsFefJiSRBuJ xNnHZZ/FVzoT7EBZ3b7NiNTm4l9A2K49C5IB4YtCbLtgR97hoUSCUOlBU9ZxeOPtN2mw Lc+w== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:date:from:to:message-id:subject :mime-version:x-original-sender:precedence:mailing-list:list-id :x-spam-checked-in-group:list-post:list-help:list-archive :list-unsubscribe; bh=2PUD1wjT144JYKET2oTTOKDbOJS0iTP3wQvRACKFgpE=; b=obh01mFkXiz47RJhzDDuNBZ8U3M7ge20DTPjWiqYoxWk2sjiPiuM0bMXs18GINDCpK jW3ue7lLquxlFRAinFhjRmnnD31/Kow956NdX2kXbcHJwRqsgf58apriHCARKbmAQCyW zpPiD7t4X/U4rzjg100AkW2wvmhrLIF4Hh/QPJ352k6ESJ+RP0knJ5KyFAAQpKecKUTs yzKol/F5OMN+DVqVQjD9yA5Yw9MgCtAbU2ghH/iQUu90pTFRhGstUvTHL1eWcNxllmSO WlHPQ8U+KNLDhvdhaldBgfV44uaxpNBKxi+9WkUkOPIswPhaxi1ecn7StnxlmXPnJHNC xjxw== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AOUpUlEn3/MMyNxl9rfwHiXUEzRE/pbs8xVjL5643YRrPWr0Hp5lfq9J VKGgZLTsNW2t0au5sIGQegA= X-Google-Smtp-Source: AAOMgpeOEC+s09HXdL1i8Z2AMRxoDSB49L4hB6Pw+zZ6Ct2GmrST3zQMshDHredKPw7iiyHNMevvXw== X-Received: by 2002:aca:4787:: with SMTP id u129-v6mr197459oia.4.1533292407825; Fri, 03 Aug 2018 03:33:27 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:aca:389:: with SMTP id 131-v6ls734719oid.22.gmail; Fri, 03 Aug 2018 03:33:27 -0700 (PDT) X-Received: by 2002:aca:eb15:: with SMTP id j21-v6mr197560oih.6.1533292407268; Fri, 03 Aug 2018 03:33:27 -0700 (PDT) Date: Fri, 3 Aug 2018 03:33:26 -0700 (PDT) From: Andrew Swan To: Homotopy Type Theory Message-Id: <5def3b96-6717-48f4-ac47-18957239c211@googlegroups.com> Subject: [HoTT] Two Papers on Path Types and Identity Types MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_620_1103885213.1533292406836" X-Original-Sender: wakelin.swan@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: , ------=_Part_620_1103885213.1533292406836 Content-Type: multipart/alternative; boundary="----=_Part_621_701679166.1533292406836" ------=_Part_621_701679166.1533292406836 Content-Type: text/plain; charset="UTF-8" Dear all, I've posted two papers to the arXiv that might be of interest to people on this list, both on path types and identity types. Identity Types in Algebraic Model Structures and Cubical Sets - a nicer version of my earlier work on path types and identity types in algebraic model structures Separating Path and Identity Types in Presheaf Models of Univalent Type Theory - in some situations it is possible to show that path types cannot be used directly as identity types (and so some kind of separate construction is strictly necessary) Comments, questions, corrections etc are welcome. Best, Andrew -- 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. ------=_Part_621_701679166.1533292406836 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Dear all,

I've posted two papers to= the arXiv that might be of interest to people on this list, both on path t= ypes and identity types.

Identity Types in Algebraic Model Structures and Cubica= l Sets=C2=A0- a nicer version of my earlier work on path types and iden= tity types in algebraic model structures
Separating Path and Identity Types in Presheaf Mod= els of Univalent Type Theory=C2=A0- in some situations it is possible t= o show that path types cannot be used directly as identity types (and so so= me kind of separate construction is strictly necessary)

<= /div>
Comments, questions, corrections etc are welcome.

<= /div>

Best,
Andrew

--
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.
------=_Part_621_701679166.1533292406836-- ------=_Part_620_1103885213.1533292406836--