From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: homotopytypetheory+bncBDF4ZP7WUQGRBDH4WXOQKGQELTG5QXA@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-x33c.google.com (mail-ot1-x33c.google.com [IPv6:2607:f8b0:4864:20::33c]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id a59a9b02 for ; Fri, 28 Sep 2018 01:04:13 +0000 (UTC) Received: by mail-ot1-x33c.google.com with SMTP id q12-v6sf5517932otf.20 for ; Thu, 27 Sep 2018 18:04:13 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; 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-unsubscribe; bh=4TAnCvA5McT3lxfjqdwoMHKQEZzu/ceV7CRpOmiqVAE=; b=gqyBckhrlxfSRzaIIbC9gtkmd5vLy78ecfINhh2Zlb8/vxgbISgwZ+s5rizkEX6MYP x/RxeOH3OII9u8Rw+Fra7YvvLTJivIv1yuuehhprdQSnFX1c7YUXsKJC6A42inbcKV2b ezvYaLOSoHxJ3+OYM0HNUEUlJAGcCVNSl/bP/PXgtQaDNsnEabMZoeGC1DHHrIaikqKI gSvdBuETl2VsKDovzXi3NRy1wKbWOjz6lhZpBccovbOzwcs1RwOj2XeaxzGfOTiigQKw W5kuXi4dTHjB//IJniu3U9dBgIXJuvoEM+K5/v6Ddxz6GUIYopoK4/pa2Ls9/y9msuCM bzAQ== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; 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-unsubscribe; bh=4TAnCvA5McT3lxfjqdwoMHKQEZzu/ceV7CRpOmiqVAE=; b=G8rm6PdBoJOb331YRei5v8XwS3FH8DG9lqR7oWK4dpB4f6Dh67JhjHFq9SOuG73Y0Z +1qPY8Ju7TXDBY7mwwmzLhtGky+52Wj36hkIjbv8oLKgOo3+rC97n8jOZ7J4noduCn0S lQ2cng4xfs6PLxuVnxD2wByjrP1ypTouCcFGJ3JSd6wMhGxAlRfVQ16vLiQ59hIpXewi 0kzNe1UFqd11H0/qX/gTQT2lldizVnnFKGaQe+ODWRJ6b9kD3ADrv+eIkP6M02cupAoE lb9VaHsqGzlftjlTyhkti9rqKQ9u6ZtNIfonJSbQLPNKHznUiEBprdwvIhFBtwMXIjcO fcpA== 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: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-unsubscribe; bh=4TAnCvA5McT3lxfjqdwoMHKQEZzu/ceV7CRpOmiqVAE=; b=F7YEEOFQf/MnHXT2Ec7+g2vquVmY7iH8ASoaUYDZKrI9BHwsRBMDMLpiumcn4wJPdv Ih73NAsD4LMD1coW91kpFq6MDu1xbtGn6jDsy2UYnsKHyicFilDzGX/hbDoe9T2rYuS9 zPj8EPPoAn5PPf9/b99sgQOK3B2IyelMkiwDoN6oD9ncc4iPqOtjZhiAvbO1EecqBVh+ j61xFM/1AZ2xI9mSFcRRifdmKwmqr2PGLYnHxIltFbGOVKI7/bbJGpicfRjLbE0zuf0/ bv+5l8GLle1zR65JDdrYmEf/b0UutB5NxGMGX1X38gXmDgDFR7XLaAe+vckVAOu5Wpo2 ahxQ== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: ABuFfoh015CDDIGLqXEGvg+MBhmUmU3hGfwtdGSp/rSujFl0uVqm7BrF Sgl4Y5haQs5Di1v4+UZu5Zs= X-Google-Smtp-Source: ACcGV61K7VNOLt9xS6LtAFY6KurTOf+nuwZNI4+hNVYpLvIBsKkbnmYGqBMr5STF2IHzV66GcByH7g== X-Received: by 2002:aca:7552:: with SMTP id q79-v6mr237517oic.1.1538096652961; Thu, 27 Sep 2018 18:04:12 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:aca:1803:: with SMTP id h3-v6ls4600753oih.13.gmail; Thu, 27 Sep 2018 18:04:12 -0700 (PDT) X-Received: by 2002:aca:c656:: with SMTP id w83-v6mr242866oif.2.1538096652748; Thu, 27 Sep 2018 18:04:12 -0700 (PDT) Date: Thu, 27 Sep 2018 18:04:10 -0700 (PDT) From: Juan Ospina To: Homotopy Type Theory Message-Id: <2f7b23f0-f395-4c31-b237-b853603cb815@googlegroups.com> In-Reply-To: References: <91b60f0a-e5e3-4216-a422-9b52bb8a4cc7@googlegroups.com> Subject: [HoTT] Re: Characteristic Classes for Types MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_85_1934687391.1538096650686" X-Original-Sender: jospina65@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_85_1934687391.1538096650686 Content-Type: multipart/alternative; boundary="----=_Part_86_201312349.1538096650686" ------=_Part_86_201312349.1538096650686 Content-Type: text/plain; charset="UTF-8" Ali, many thanks for your comments which are very instructive. Actually I am trying to understand anything in the Floris van Doorn's thesis, particularly the formalization in HoTT for the *Atiyah*-*Hirzebruch spectral* sequence and the *Leray*-*Serre spectral* sequence. > -- 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_86_201312349.1538096650686 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Ali,=C2=A0 many thanks for your comments which are very in= structive.=C2=A0=C2=A0 Actually I=20 am trying to understand=C2=A0 anything in the Floris van Doorn's thesis= ,=20 particularly the formalization in HoTT for the Atiyah-Hirze= bruch spectral sequence=C2=A0 and the=C2=A0 Leray-Serre spectral sequence.


--
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_86_201312349.1538096650686-- ------=_Part_85_1934687391.1538096650686--