From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: homotopytypetheory+bncBCXZJBXDZ4ORB2FAWDOQKGQEZ7DSZJI@googlegroups.com X-Spam-Checker-Version: SpamAssassin 3.4.2 (2018-09-13) on inbox.vuxu.org X-Spam-Level: X-Spam-Status: No, score=-0.9 required=5.0 tests=DKIMWL_WL_MED,DKIM_SIGNED, DKIM_VALID,DKIM_VALID_EF,HEADER_FROM_DIFFERENT_DOMAINS, MAILING_LIST_MULTI,RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.2 Received: from mail-pf1-x440.google.com (mail-pf1-x440.google.com [IPv6:2607:f8b0:4864:20::440]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id ab0137dc for ; Wed, 26 Sep 2018 23:04:10 +0000 (UTC) Received: by mail-pf1-x440.google.com with SMTP id i68-v6sf698178pfb.9 for ; Wed, 26 Sep 2018 16:04:10 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1538003048; cv=pass; d=google.com; s=arc-20160816; b=AyZG0sFM7MvusbchRmKXwr4cZHlzBwpqzmof1yuXqSjbKIbzyS7bIhTMfSPhiPFaFs 596XWnr+9eustuesZlUPJ5QLAgoigrCej9TZa9J5WMLI6RRz3eReS509EfclbiSOeddz 5R2gEbAzpJmjEMu+kYF04KqBuSXvARJ+od3ETskHTWjuRpAXlhuwNL7ksMIO2VOlBnBr /k+knXeop6SL7+xVZnrIOmLrNGSR1VaB7Z/h0u+5bbt8yl29Y87VyfUq6xMlxLUsPc5s hE6paPZ+0wJArKPzq93udwlMQJU6sL6oQtzrpbfhHBrgdVH8TX17yBMy3rKeMCEzSDfu /8hA== 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; bh=qnq6f4am7GlW83ukUhpcwWmjQgIUD5crO3cVo2crApQ=; b=aH/DNWV6vePIoYcTUSLmxBVxJtN9Z/cnC3RZ0qS0NwpSne9nGUzvIR/yc6gxJTrNRb IbRJ9G6I0MLSCen6BYeZCVj3ty8Dyj66/FkXNpyrLKYDve+0MIc2zAYtfG+5xX7rqMpw jdaEX6W6xMtqxUNVhF/8IvmvJ23UdQSu1Wdzwm/TV7dL19KplK3+F2c0QgpgwA62A5e8 g48aTPvRx/igrHPy8mW9KZYyYvPjKOqpO5zkYmfuq+yMeV7MSd8K46oBUOd5Hlbw5kcY kLwDOigA3hdeB26MldaED8DsFZW9NZZvlSl7S6CBbCSLDtknRAwy0ckHNZo/GSnIcUwa xY3g== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=0B+y3QES; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::b36 as permitted sender) smtp.mailfrom=shulman@sandiego.edu 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=qnq6f4am7GlW83ukUhpcwWmjQgIUD5crO3cVo2crApQ=; b=YgJxZ0XhRnxVWynI985E7L4kwhSFbwaabihfPNOdYdRtbVxSAjfLAHYLfummRqOuO4 0wYXCUkn5XG9xSZ9vlXOdIGs5D2bSPAxpQAaYdyKmARNWjiW12VGIjywqwD3KS/Hn/05 Gh2ROpPTegZO9I4wWa86NWXJaWVbpzW8Q9eaU7aHR6yTsPz7QYtA4PzDiX9gu0s6llaV piheO+ZmoCq2bqGFWodBFuAjhY5Snpd6OfgTCC6O7Vk0oB3k4ByNiXRXMa2ttIonph0M NlmQ/9iKNj10QSW+hpGG2UAyiHAlQppLB+xp1LXVqLokZysam6URIVxmaQ/P/VPPjgCe H5kw== 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=qnq6f4am7GlW83ukUhpcwWmjQgIUD5crO3cVo2crApQ=; b=PWafKxFckcSyVwW9rRkmMRbHkjvqPKMmwkozXPkdYDb9cNSOr2ljDkkslgl+Y9CJqR PARMGHymXAtJUN1GZOTbxZujU2pDICltJh87aWseStEIzBlvLVocoAMCAiBTEeDU12fQ uhkS/+4sOPUk2vR+Tgl6/lmVQNX5rYtihKprJ6aUsHNZnlXmtklVLKzAHB6ng8tT72o2 TP1bY9T1x9apl0t+tbwyK2jkhHmMp9pdpKJ55tQBQP5mzA5chJfd1f+nkQO1iQHqFTHm PNndPj08lnQrzYdLZ5JMrMDOQ4rdLCrA2YXxFbO8Ir1/ej3xhPbi7+wz5KyKATE/tySp +Omw== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: ABuFfogvrF4+zjQ2XhVlHXtGxWBfJH+ZZDUP9weRMl5EaUry5vqTb2la fO9mkBEnszWRYMNl+3QuDuU= X-Google-Smtp-Source: ACcGV631kGbDgeTgl8TQI8wkonZ3Fiv1OmIaIduvNA2+Z0+i2qIC+RjbhZ5IRn/2muZcqMTVg9lvCw== X-Received: by 2002:a17:902:7887:: with SMTP id q7-v6mr30413pll.4.1538003048468; Wed, 26 Sep 2018 16:04:08 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a62:fb01:: with SMTP id x1-v6ls1113209pfm.9.gmail; Wed, 26 Sep 2018 16:04:08 -0700 (PDT) X-Received: by 2002:a62:b0b:: with SMTP id t11-v6mr995809pfi.24.1538003048119; Wed, 26 Sep 2018 16:04:08 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1538003048; cv=none; d=google.com; s=arc-20160816; b=Fg4DmNCNTNUfPlUx+9Z3VB/y/soiyj9FqCQIHoDrLF42QUKDQ+IqFveoHE3Ln0isgk PinjWZQDx567etCCMUQX8oVSkSO5x1pWPUTE+4MIvWSi2cJUDFfIrPOXC3WFXN7vTOMN 7fI1Rh2E6ODQoHNY06ay8+f/L44ybWmZ8gsHhnAho/Wcx8PYhBV3JFYwjhCeGWJzNSK6 cK3SZhd4x9ZfY0Ewo9bgmcBvBvLInOdLSzhwWOQk0g3ZG5fJAg/DeHLLdO00MlTBDLXB 1CXl8T6liACfbo3OcMFwPWybLrtuUIqH6KjpYKolBlR7LymUROr+0s9ObPQX1gZ19b44 vHiA== 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=zSexRjdXwx9GB/Cy5L67GY+h7NdfQiDJJx/un4VP4TU=; b=U9x5yYGUsbwVcWqGZuwj15wgNhI2DinTZpampYxWGT54KhsJinaNWuN6EpZ+jsrqrr hw07nQZZb5nOy2LtqdBtcF0MaTPi1bkFppc0BbCWi/CfxTm8QEC68VWAOU4qp0ArPfg8 faA1uIHqrisOvS9l0r2TSKX73s67pj63f2oy1+qy07qbiPl6wT8SRp3DmkIDda1njchQ Cw7e71r3z350vMO42XTv20kwIZ+HtwBA598mGaMM5yW6dyPWeKXnn0KoH6Pd7+B8mEVO qRYKnAxBehYo3g0QCQdKWR4rJROyQ5L8lWdz1N6oftQn72HRfkBWIsRcqoAR94seDFQ4 wNXQ== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=0B+y3QES; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::b36 as permitted sender) smtp.mailfrom=shulman@sandiego.edu Received: from mail-yb1-xb36.google.com (mail-yb1-xb36.google.com. [2607:f8b0:4864:20::b36]) by gmr-mx.google.com with ESMTPS id y64-v6si8506pgb.5.2018.09.26.16.04.08 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Wed, 26 Sep 2018 16:04:08 -0700 (PDT) Received-SPF: pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::b36 as permitted sender) client-ip=2607:f8b0:4864:20::b36; Received: by mail-yb1-xb36.google.com with SMTP id c4-v6so300302ybl.6 for ; Wed, 26 Sep 2018 16:04:08 -0700 (PDT) X-Received: by 2002:a5b:346:: with SMTP id q6-v6mr4352759ybp.193.1538003047605; Wed, 26 Sep 2018 16:04:07 -0700 (PDT) Received: from mail-yw1-f51.google.com (mail-yw1-f51.google.com. [209.85.161.51]) by smtp.gmail.com with ESMTPSA id a145-v6sm259971ywh.100.2018.09.26.16.03.59 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Wed, 26 Sep 2018 16:03:59 -0700 (PDT) Received: by mail-yw1-f51.google.com with SMTP id y14-v6so305967ywa.4 for ; Wed, 26 Sep 2018 16:03:59 -0700 (PDT) X-Received: by 2002:a0d:e341:: with SMTP id m62-v6mr4196289ywe.421.1538003038822; Wed, 26 Sep 2018 16:03:58 -0700 (PDT) MIME-Version: 1.0 From: Michael Shulman Date: Wed, 26 Sep 2018 16:03:47 -0700 X-Gmail-Original-Message-ID: Message-ID: Subject: [HoTT] A communal proof of an initiality theorem To: "HomotopyTypeTheory@googlegroups.com" Content-Type: text/plain; charset="UTF-8" X-Original-Sender: shulman@sandiego.edu X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=0B+y3QES; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::b36 as permitted sender) smtp.mailfrom=shulman@sandiego.edu 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: , Hi everyone, I and some others are planning to work together on the nLab to write out a complete proof of an initiality theorem for (to begin with) a basic uncomplicated dependent type theory. More details are here: https://golem.ph.utexas.edu/category/2018/09/a_communal_proof_of_an_initial.html Anyone who wants to join us is very welcome! Please just add your name to the list of participants here: https://ncatlab.org/nlab/show/Initiality+Project and we'll probably start work in a couple of weeks. Mike -- 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.