From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: homotopytypetheory+bncBCXZJBXDZ4ORB5WLUPPAKGQEKO3HJBQ@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-pl1-x638.google.com (mail-pl1-x638.google.com [IPv6:2607:f8b0:4864:20::638]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 592227c1 for ; Thu, 18 Oct 2018 19:58:48 +0000 (UTC) Received: by mail-pl1-x638.google.com with SMTP id f5-v6sf23833151plf.11 for ; Thu, 18 Oct 2018 12:58:48 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1539892726; cv=pass; d=google.com; s=arc-20160816; b=O0ZMZWeZDEusGFH3K7ZzphTPZI2h1VqwQUVraAerIdYdE3YHV+I9X++jF+5wkTa2Z1 d/ktOmN4JsRGbzPEwOijzW3uNYmxiFDh9CTrtPlWUSHcIL1ZLdk0JrsWeOgtZup2tALR 33ZJN4/TsohNHjUiWZe0/Fa1o9zN/lheNkXVlUBVTi3g6vywqYRGXYgWJB0on8ngAw2J wjQuSklRKoy7OmwWqT3igM0DfNGu/OwxGpONOFI6ya8N8E/4hVuRbUpAE8pHSBGfIJlM BWPX+hr25xAHrvM5NUY5NS2xdeDGblZO+11LA1aCZCcaK3aPPoshnYLZcK26WcArcJ8M J7Xg== 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:in-reply-to :references:mime-version:sender:dkim-signature; bh=al5na94iCtp/F/DpfUAxhAIeUU5a+nVaZ68repBEDJ8=; b=PyQDVF0hAhyaf+RFYQobdUJAMBBR+nMpbDwDdIKKZ0FnkgqJr5qax8YGGH3AzG9+R7 LCaW9Ksk/otpstYMq/0iIfQa9YFrZATOuUwsCSywsiq8IhINAScWmko0BzinHC3Drmt2 Dn9Ix3tLVcBstvWFMD7Wkyqjf/9tnOWm994tWBtZoMMBiodRkxGAyBUV7hZrDHkVJeYs T/KviNMg+H8EunL5RnzLRNkHFsweW9LQLhzYaTZYlxBJGu9bRHEY2Mzd2EPnolCX/hh2 MWo/Xkz045/lMmwAu3BhUkc+h8boukMxXdjq6ku31OoUVeyhz71bkZuZDMBS6ddtgRkz F0ow== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=NOAlWZJ4; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::b31 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:references:in-reply-to: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=al5na94iCtp/F/DpfUAxhAIeUU5a+nVaZ68repBEDJ8=; b=Qy+tv2nFHDDlTz8Nk3ytV8X4yD74pgVCypOCy10sAhUhgLSLIrQgpfowYpx23TYSF3 ydBbMtt5e8tS075QN4p5hAFN7An3rfEughoj9x7zDcRJ6AwvdpxEJ7iGZxnzyx6UO9pT w3nlvlFQsN3JueGFeSWOQScF/7Lc7kzYgOi7cuHY3DwvTdX+Z+QQ+v9YhJf5ojFCjbpi +NXKupXUyu6RNgRFVJz8ROhG5B1r4yvXxLx/opL2g+NIyXrSOqSPXqi+iUUqLb2BxmrG k/QFa98EgVPOSJcHhlGUnEQruH+a1Jl00+4QgjaO8feWzUq44lqljxDKF4BnasvkMBas YeOw== 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:references:in-reply-to: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=al5na94iCtp/F/DpfUAxhAIeUU5a+nVaZ68repBEDJ8=; b=lbFC7tZLWE7/r7YAbIlNYMG1mVImjiaB0QSI5UX9WZq2osqPhNlTD5UQVtzSPHhrwB VKsqrMZHxtfjm7jWoKU9T3eQbtqeg1XrmJWh/PW9ZwNUryRWB5cX7gy0dP7ZSwn/VbXv mjzDA3LizvBVizoGojvdshmjM7GFOXXhmKKQ7NkVj48fhSPr1dV9/sPCvflAXSKuLMhY RjWvscD+2p7T7PVp8gzG9zuFShpZeFHsElbsWUKCF11vC4Yc4sjMXxCjrHJQFb6stmol Ggj2lIUXkCVstc3zt7/FTnD6J+qiY4GO2zxYDMVhTeRn+T6JIRMWVfJMtFtD+XCGq7no o61A== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: ABuFfogToj1HRStSMhiZgcT4kkHVOBQDZa4Dj1OCZYRyCfRrbojtxscs TsIu1NY4FFTcHGA6E0g/GRo= X-Google-Smtp-Source: ACcGV62HUkneR0n6+CPhcAapfxA4tgh/PoRQmJjwuINzmFa2ycJiSp6L+XLhHk8+1aD2Y4IHEWmUKQ== X-Received: by 2002:a17:902:8f84:: with SMTP id z4-v6mr2151plo.0.1539892726772; Thu, 18 Oct 2018 12:58:46 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a62:ca54:: with SMTP id n81-v6ls8895512pfg.9.gmail; Thu, 18 Oct 2018 12:58:46 -0700 (PDT) X-Received: by 2002:a62:1186:: with SMTP id 6-v6mr11799159pfr.63.1539892726350; Thu, 18 Oct 2018 12:58:46 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1539892726; cv=none; d=google.com; s=arc-20160816; b=d0hNtfvZ9DE1sb93GQuWjfFcIGUihVG5mFRMIBxn+zw6HFQDb96vtJEuGWIN8E2hx2 HONu9tlyd0LTTZnAe0FwGNUwMHZIcYWa3RM/l5WCKbOwmipCCXq0f6F21VI7/c/Qzeoc 9TWIC9uNIHTHTu8rxHZlZLiJ4jGid8IaxCxilIkfMOwggfwAyLavHFzp9BwryQRxPeCW 6AJXBSsMQM2lyQqZNAQpZdNsMlC95/pnlbauGB7xRIoztUriYsl1h0eb8IEvVFGxPZY4 IVwElZ8X/Kcjgm6UyI8uJvJ9rZ4e9/8jGim7NpWwhiq8YmVV968tBmGKgIO4Gxnhh8o9 OW7Q== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=to:subject:message-id:date:from:in-reply-to:references:mime-version :dkim-signature; bh=ir0wlIdF/FSyjBJtw0mtBU2AtK/xFDeaFBs58w4ROm4=; b=DnCT2LiTF7Za4Q9is81818+nvZdNrApPLZwEuCCuPdvrz3mX7czWyT3qNF2TB/r/OV SabAsAoOrYyXjN9/50cyr/cElrxjdV+llhKgbe9gS1SdbaehvEwnAfJeKN3E1HPHRyKB aSpt8UQ8LuLQ3ioSbXigB4dgWhKCnSxKMuthUH3xLiaSEPzBYE49w9ZguBaMBH3DauGb GuQvANKcV3gqwHjOvJVRZj9GgTZz+VAxpyiYjBW0MD05rVxyyvKL7DdfMgh4+LYQpvK2 h3L2wlgQGcP0776Qs5GyBDe0Y2CniltgPlfCFaS0UUQdwOpypnEjqC0P3q4qopsMYx/1 MNHQ== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=NOAlWZJ4; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::b31 as permitted sender) smtp.mailfrom=shulman@sandiego.edu Received: from mail-yb1-xb31.google.com (mail-yb1-xb31.google.com. [2607:f8b0:4864:20::b31]) by gmr-mx.google.com with ESMTPS id h13-v6si1121902pfd.2.2018.10.18.12.58.46 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 18 Oct 2018 12:58:46 -0700 (PDT) Received-SPF: pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::b31 as permitted sender) client-ip=2607:f8b0:4864:20::b31; Received: by mail-yb1-xb31.google.com with SMTP id j193-v6so1100585ybj.6 for ; Thu, 18 Oct 2018 12:58:46 -0700 (PDT) X-Received: by 2002:a25:4a02:: with SMTP id x2-v6mr18085941yba.72.1539892725870; Thu, 18 Oct 2018 12:58:45 -0700 (PDT) Received: from mail-yb1-f180.google.com (mail-yb1-f180.google.com. [209.85.219.180]) by smtp.gmail.com with ESMTPSA id l138-v6sm6585056ywe.50.2018.10.18.12.58.45 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 18 Oct 2018 12:58:45 -0700 (PDT) Received: by mail-yb1-f180.google.com with SMTP id m184-v6so1272824ybm.0 for ; Thu, 18 Oct 2018 12:58:45 -0700 (PDT) X-Received: by 2002:a25:2986:: with SMTP id p128-v6mr7145749ybp.458.1539892724953; Thu, 18 Oct 2018 12:58:44 -0700 (PDT) MIME-Version: 1.0 References: In-Reply-To: From: Michael Shulman Date: Thu, 18 Oct 2018 12:58:33 -0700 X-Gmail-Original-Message-ID: Message-ID: Subject: [HoTT] Re: 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=NOAlWZJ4; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::b31 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: , The Initiality Project is starting, with close to 40 participants! Discussion beginning here: https://nforum.ncatlab.org/discussion/9160/initiality-project-plans/ about all the choices that need to be made at the beginning; after consensus is reached we'll start listing tasks and volunteering for them. Anyone wanting to join in at any time is still welcome. I'm not planning to make further announcements on this list (until we have a proof to share with everyone), so if you're interested you should follow the nForum threads and nLab pages. On Wed, Sep 26, 2018 at 4:03 PM Michael Shulman wrote: > > 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.