From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: homotopytypetheory+bncBCQ657FO5MEBBYMJ7DOQKGQEB55MFPI@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.7 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-ot1-x340.google.com (mail-ot1-x340.google.com [IPv6:2607:f8b0:4864:20::340]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id d99b2369 for ; Wed, 10 Oct 2018 13:55:47 +0000 (UTC) Received: by mail-ot1-x340.google.com with SMTP id s68sf3644693ota.11 for ; Wed, 10 Oct 2018 06:55:47 -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=oxYKGIOA6O0nAuD9BFdUgvJqD/aLpJjE2/6Q1IWpFTI=; b=WIuncGw5kJfa8974lVyvoc1hpozw/K3sBCA3mqqr4lGfbdJyhGiHaTfPzShBhVUGMO MMQGnfmOoYUZBdb4hjSLUJlj3EgaHaupA2URoj/2H3gZrTuAlFNITXm1+ilqJgzFsRJY o6FTUKPaCxeaAKVndxjp90bhMhxwFFJWaf4gw55wu9cFTksJJGk3ltjUV0P4JNAus83W b20gDGDAfjK8TGVh2+j05Y34ejidqsJTfqicTH5u7CzSyrBi+N4lBix2WWBeXem+7K67 /BxqVuaE6uz+XwcV1a7MDy9DoxqHnOMESsy5jC/NRdAl7iugPbQKli8Vaap/mFYWU0Ui KaYQ== 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=oxYKGIOA6O0nAuD9BFdUgvJqD/aLpJjE2/6Q1IWpFTI=; b=ThQm6kpzUIbcpVkrzu7Kg5XBo9tatCliSAFK1g77KcuMq/xC/Ku7tYpObQO6w+l/T4 id3ZVPiEmLxmjqPw9Bx3afVkO6y8Xp9sMKItjZ9jXDQHUzQjkhQjAhWDSp9K3RrIjR0R aKFYBBSmcsLT7b2mJeD4DsR33RYqc7/8y61NxsF3HcTNQeoWvmqfaRR6iNh0hkynt5CK 9cIojHlyNbrTAblqYOobONuqEX0BiQU4S+re7ybg/C8LaPgk1RRhJ/2sK+Nq+sWZ24yK g4Jjj9s4GkzPv1x1vnuWOQ/sYERDvDben+Xh2zw7KQO/qbAPKUoFxnjGB3UM4jhdCpry SEcQ== 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=oxYKGIOA6O0nAuD9BFdUgvJqD/aLpJjE2/6Q1IWpFTI=; b=kUSHq5oO5bMU2msdBKdimjRYBcs8Cj7BNnOdfJ6geWoy36UPE42bOXHUQqXg9KwLLO fKVdmHOSRaDLE5I9lHO4GBtVcf8VGIlsOIeFgGQuiq7tofiaaTs0tYwD9Ui9QkAIFuyv GvoXI3qu8bqc4e2eM5KyZ2yB3mUvecJ4nO/N5dvj7pU5rhTAYvxMrK/oVq9ljiUrvzZG +NLTrIb3jSkJLTszLfXFSOM12SRczrpva/RwGKqCPZrwSmFJhmsZ6/tq3lxZiiTH23j9 FJDMKQ3jtkNbscgusaGDAfAl6fz4U5Qld4QKzkstijF95yZyqP3lEzO/RLjSeTtbzNpz VW/w== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: ABuFfogkZnStSdLa7yS/p4ghmmRCegv9723E5QBRYEvHbWKCQT5Sj9I9 YrjxEOTvcTt2TrvxLHhsah8= X-Google-Smtp-Source: ACcGV62yhfwJUAhawUFDZaEH3HOcjf5ZkZLiSN2UWUz92D6M9bfb/HWu5pfxY3pKx4J07AOmBMdsDw== X-Received: by 2002:aca:eb91:: with SMTP id j139-v6mr571047oih.4.1539179745583; Wed, 10 Oct 2018 06:55:45 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:aca:eb81:: with SMTP id j123-v6ls3802966oih.4.gmail; Wed, 10 Oct 2018 06:55:45 -0700 (PDT) X-Received: by 2002:aca:3094:: with SMTP id w142-v6mr566393oiw.0.1539179744972; Wed, 10 Oct 2018 06:55:44 -0700 (PDT) Date: Wed, 10 Oct 2018 06:55:44 -0700 (PDT) From: Ali Caglayan To: Homotopy Type Theory Message-Id: Subject: [HoTT] HoTT Wiki MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_2507_733392749.1539179744375" X-Original-Sender: alizter@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_2507_733392749.1539179744375 Content-Type: multipart/alternative; boundary="----=_Part_2508_822524968.1539179744375" ------=_Part_2508_822524968.1539179744375 Content-Type: text/plain; charset="UTF-8" Over the last few months I have been adding to the HoTT wiki , just contributing known facts from the HoTT book and reorganising a few pages. There are a few pages that you can use to find the others: - Synthetic homotopy theory this is supposed to detail known things about synthetic homotopy theory in HoTT. There are a few references at the bottom consisting of PhD thesis' which I mean to go through and add to the wiki. Sorry about the mess. - Category theory (in HoTT) this is following the HoTT book essentially. But this shows the potential the Wiki has for being "the ultimate HoTT book" given that we don't have to publish anything, there is not limit to what we can add. - Type theory this is supposed to detail type theoretic things, i.e. the first few chapters in the HoTT book. It is in a sorry state at the moment. There are only 100 pages or so, you can find them through the All Pages link at the top, furthermore, you can organise pages by categories (still WIP). Now if you are reading this email you are probably interested in HoTT in one form or another. So please contribute! You can get a gist for the general style from the articles I have linked. Even the smallest of contributions are welcome. You can post on the nforum or email me if there are any substantial issues with what I have written so far. Ali Caglayan -- 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_2508_822524968.1539179744375 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Over the last few months I have been adding to the HoTT wiki, ju= st contributing known facts from the HoTT book and reorganising a few pages= .

There are a few pages that you can use to find the oth= ers:

=C2=A0-=C2=A0Synthetic homotopy theory= =C2=A0this is supposed to detail known things about synthetic homotopy = theory in HoTT. There are a few references at the bottom consisting of PhD = thesis' which I mean to go through and add to the wiki. Sorry about the= mess.

=C2=A0-=C2=A0Category theory (in HoTT)=C2= =A0this is following the HoTT book essentially. But this shows the potentia= l the Wiki has for being "the ultimate HoTT book" given that we d= on't have to publish anything, there is not limit to what we can add.

=C2=A0-=C2=A0Type theory=C2=A0this is supposed to deta= il type theoretic things, i.e. the first few chapters in the HoTT book. It = is in a sorry state at the moment.

There are only = 100 pages or so, you can find them through the All Pages link at the top, f= urthermore, you can organise pages by categories (still WIP).
Now if you are reading this email you are probably interested i= n HoTT in one form or another. So please contribute! You can get a gist for= the general style from the articles I have linked. Even the smallest of co= ntributions are welcome.=C2=A0

You can post on the= nforum or email me if there are any substantial issues with what I have wr= itten so far.

Ali Caglayan

--
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_2508_822524968.1539179744375-- ------=_Part_2507_733392749.1539179744375--