From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on inbox.vuxu.org X-Spam-Level: X-Spam-Status: No, score=-1.1 required=5.0 tests=DKIM_SIGNED,DKIM_VALID, DKIM_VALID_AU,FREEMAIL_FROM,HTML_MESSAGE,MAILING_LIST_MULTI, RCVD_IN_DNSWL_NONE,T_SCC_BODY_TEXT_LINE autolearn=ham autolearn_force=no version=3.4.4 Received: (qmail 15293 invoked from network); 24 May 2022 09:49:39 -0000 Received: from mail-yb1-xb3a.google.com (2607:f8b0:4864:20::b3a) by inbox.vuxu.org with ESMTPUTF8; 24 May 2022 09:49:39 -0000 Received: by mail-yb1-xb3a.google.com with SMTP id m9-20020a056902004900b0064fb755258dsf5787571ybh.13 for ; Tue, 24 May 2022 02:49:39 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20210112; h=sender:date:from:to:message-id:in-reply-to:references:subject :mime-version:x-original-sender:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-subscribe:list-unsubscribe; bh=JnnuOzTvRGHsRdSgmCvQ+egNRNRRa9wzrBfOhLRCEzw=; b=I07r7JcPXUJuoD6ANWMxo5I4XE16dPblE2wNra/4ENjpvJsPt0a6h+7NC2HSP7Wx56 gxGxjLbv+wjdFOwqxGSZTXPFGggZrgKY7m23jg+fXwlb8Lpl2gDnKY6Bn/Ikr2R+4m2m yq51i40cTO+suLW08slwzM48+YMPFzp3j0jwBFJt9rxGHPfvySxkliwqumydsZHxj5Ez Po1RMP7Uw72N6awQVGQYaj1dNpQae+ima131QC4Fjm8a2PtMcYvgYVIzyEAS7OB25a4U DWa80dm0p7KfsObpZUsiPNVJkvJs02c4bE2t4VORnOHug+9HcShar3pBOPAR6ysmDe48 0BPA== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20210112; h=date:from:to:message-id:in-reply-to:references:subject:mime-version :x-original-sender:precedence:mailing-list:list-id:list-post :list-help:list-archive:list-subscribe:list-unsubscribe; bh=JnnuOzTvRGHsRdSgmCvQ+egNRNRRa9wzrBfOhLRCEzw=; b=gISodlRBg9VSKxWiss36h6871F2dBibv1mUgrUM12jMhh0Rtp6hMYZJpTrzrZXkSx7 Z4R+GG39igtvkDfXnSuBm+ylLxSoDc6DwhN7bjig8jg9S9xjlHfVzXapEEA/2S1ZxeV1 B2MRMev3NYOW+d3ccsn/nYajeKcipsoLqGg0EVzHF0q4AI8yXC7krbdB565NwZ57OwHW w/DwLoFw3uC7Mi83p1J6qr/fytX1Yy7dEigNE1E0Q6PlOCDGajuqCoT3AwHpu+ObDu8N CcUpPNNx7fG9euYbuVofd5yPWnY2JT0kKEthej7SAPHxKl8Gjro8zkViXGKmexkw5Agz qAyA== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20210112; h=sender:x-gm-message-state:date:from:to:message-id:in-reply-to :references:subject:mime-version:x-original-sender:precedence :mailing-list:list-id:x-spam-checked-in-group:list-post:list-help :list-archive:list-subscribe:list-unsubscribe; bh=JnnuOzTvRGHsRdSgmCvQ+egNRNRRa9wzrBfOhLRCEzw=; b=weuGtIMMxZ/cHBGwNubCDQR3TwnXa0hbOZppwDmZHI10pRFUKymOf0///9RxOOqBxa giUIr8vIXgLVZ8+vyEkiGSKmXdVbYVZ16hBqNO84Tw/UdvyqScvAePYA/KZUUw3Uo5IF isod4U4MbFo9QBTGZZTHc9QYOKE1lcge0BPEgt1akjMC8U0M2pjjZEYg+jaP+LZKBTAu 3iBaQVf6l5tZnRk0mLLIlQ/2lC1ZgDKse/G3iE021nj35onHS/wsDoMwiewXVY2hoARa PQl9UqD/T4fGY0MGEZOmzGJevxNGHQJVrZZFg4xDIvE21vqEJ2KHdgF8r754/6fKLt8S cYJw== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AOAM532qlVBzNOcE0osTeRN1EiRYu/9L1eSCnJcTEX1FbLpMjzX5f/6T b8qpl4sIwvaGDXvytwUshxA= X-Google-Smtp-Source: ABdhPJye8o+FxpEv8oVXwZAv2GCtUEx2ZIulwYeq3hBLtUcHkxyo4Opq88I3520PXzZn58iUy0Muiw== X-Received: by 2002:a25:e708:0:b0:64e:a3ee:ef89 with SMTP id e8-20020a25e708000000b0064ea3eeef89mr26655376ybh.164.1653385778393; Tue, 24 May 2022 02:49:38 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a81:fc7:0:b0:300:2820:4c3 with SMTP id 190-20020a810fc7000000b00300282004c3ls772292ywp.0.gmail; Tue, 24 May 2022 02:49:37 -0700 (PDT) X-Received: by 2002:a81:ed4:0:b0:2f1:c8db:ce23 with SMTP id 203-20020a810ed4000000b002f1c8dbce23mr26739432ywo.95.1653385777347; Tue, 24 May 2022 02:49:37 -0700 (PDT) Date: Tue, 24 May 2022 02:49:36 -0700 (PDT) From: =?UTF-8?Q?Anders_M=C3=B6rtberg?= To: Homotopy Type Theory Message-Id: <78088eab-9b8e-4dc3-a2cf-91ae4aa3b5cbn@googlegroups.com> In-Reply-To: <36c1e828-af3a-49c2-840b-1fae9897eeban@googlegroups.com> References: <36c1e828-af3a-49c2-840b-1fae9897eeban@googlegroups.com> Subject: Re: [HoTT] The Brunerie number is -2 MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_202_2105858265.1653385776799" X-Original-Sender: andersmortberg@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: , List-Unsubscribe: , ------=_Part_202_2105858265.1653385776799 Content-Type: multipart/alternative; boundary="----=_Part_203_1022642985.1653385776799" ------=_Part_203_1022642985.1653385776799 Content-Type: text/plain; charset="UTF-8" > > > This was before Cubical Agda was invented > > Oops, I meant to say that this was around the time Andrea Vezzosi was implementing Cubical Agda (which Guillaume mentions in the slides). -- 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. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/78088eab-9b8e-4dc3-a2cf-91ae4aa3b5cbn%40googlegroups.com. ------=_Part_203_1022642985.1653385776799 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable

This was before Cubical Agda was invented


Oops, I meant to say that this was around the time An= drea Vezzosi was implementing Cubical Agda (which Guillaume mentions in the= slides).

--
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.
To view this discussion on the web visit https://groups.google.c= om/d/msgid/HomotopyTypeTheory/78088eab-9b8e-4dc3-a2cf-91ae4aa3b5cbn%40googl= egroups.com.
------=_Part_203_1022642985.1653385776799-- ------=_Part_202_2105858265.1653385776799--