From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: 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=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-oi1-x240.google.com (mail-oi1-x240.google.com [IPv6:2607:f8b0:4864:20::240]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 63bf1725 for ; Tue, 16 Apr 2019 12:06:13 +0000 (UTC) Received: by mail-oi1-x240.google.com with SMTP id s184sf9716753oig.19 for ; Tue, 16 Apr 2019 05:06: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:subject:mime-version :x-original-sender:precedence:mailing-list:list-id:list-post :list-help:list-archive:list-unsubscribe; bh=xSLcCXlLIXjNBbpQTmFpL2fDQOx+PQXYz2rsD/trB3E=; b=RJPsItaalsYIKaH3I+pJ+NVIWAJQGyzZeEtXdNW3m8SdCzSDjX52NN275lUHawLi1p JHg/QvtUJMO+pMcYaNyJ2mK9oKIwgl8Mh7y5p8okC2PQIZskgxSa2LDOSZSwijijJzta ANIGoADbEPQ1oAkB3s7paOCCBJrG/kCVLQs9dAk9h7ewO5a5aFPq6zjcI7GMgZdldZvd fx2N/t0WromZnixJr28MvOWCkxNDDx1WAluv7w+KSz7p/AVhb/iowQYbt0dfvXhHVqDG kwd41OxQ+ClLTViOLIy0mZ4Iz2XsIRvrnY8KySq3Bl9/kwc2qCkfVglo4k0c/vREYgkT CRgA== 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=xSLcCXlLIXjNBbpQTmFpL2fDQOx+PQXYz2rsD/trB3E=; b=WBSIpxj5IEy5UV378g0J5qEXwsJKPNupNaS2Bjnn0dBwMuSPgI5oyAXvlFQmQxrwih 8whX2176Z2oSxphxDYlBilkvsmbC//fpzcjjzWFAgBgECKr4DDogxcgpkNp3r8lpxdoE 96hrF4e5Xl7J0qTxoNoYY4eBjGeQ89iDP1vXsZwwCN9sVKq92ZYFTDQ+Ueigv/rSaNhO fmxJ/xp6M1uldAF0Az4ggN2L1Ds8MlUOYLV3KcvPswqD9AsJB70wdo6EDHFTu02+yfhR Q101wJ7Cei53n8kugKumelEzSZwfHExUne8zd+pkkocThUs3KC/vHNcO9nwUqzv9kgzV 2HjQ== 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=xSLcCXlLIXjNBbpQTmFpL2fDQOx+PQXYz2rsD/trB3E=; b=PBqRTcfrNOrRvhEDn2Frf9ITfkEW1/s5bwddXX7/ea2h5g0dHfD8lwAkTK98ymUcII C3asH3pF7wnpwWYrZaz/+9hwwRWR2kc0f2J4SUJEDaTjaMRTvzI/OLRViOhwchjxLKrN gkzN6SDG6fBTYKokpAyT9U1PWiFi80QQQ2sp30SJ423BnnHjcK48go3rUesxuUfrPURJ 9KfHv8cjb+9QZouXPHmKjwop9mo9JJYilGhT/VgYgb/Mw1QTngjFahkJUMAZ2zVRMf7s TaivZiil056NUEJfBwCUNICi3p9Bx5hWGb09RYaEcXq2gwU0Ot6uPMICBgMDdSYn6Fy5 Ccxw== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAXmbRo0k+s9SNBnr8as8PvKlkfFaSCksu/+EIMHm2lcORHqolKx E+QATJH/ivuSxtj6anfGyRs= X-Google-Smtp-Source: APXvYqzhBLKff5L5A11pned6R5xEcdlY+tjSEV5LyNgNfzRtj+1KY49SSxOdlbm1HPXeYZMRZ6IGcA== X-Received: by 2002:a9d:6ad1:: with SMTP id m17mr23690243otq.108.1555416371625; Tue, 16 Apr 2019 05:06:11 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:aca:88e:: with SMTP id 136ls1559044oii.3.gmail; Tue, 16 Apr 2019 05:06:11 -0700 (PDT) X-Received: by 2002:aca:3946:: with SMTP id g67mr19493083oia.28.1555416370652; Tue, 16 Apr 2019 05:06:10 -0700 (PDT) Date: Tue, 16 Apr 2019 05:06:09 -0700 (PDT) From: Ali Caglayan To: Homotopy Type Theory Message-Id: <655fcacc-0d88-47f7-bcf6-3a0e27ea10fd@googlegroups.com> Subject: =?UTF-8?Q?=5BHoTT=5D_All_=28=E2=88=9E=2C1=29=2Dtoposes_have_strict_univalent_uni?= =?UTF-8?Q?verses?= MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_2191_1828964353.1555416369923" 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_2191_1828964353.1555416369923 Content-Type: multipart/alternative; boundary="----=_Part_2192_836104702.1555416369923" ------=_Part_2192_836104702.1555416369923 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Mike has released this new preprint on the arXiv: All (=E2=88=9E,1)-toposes have strict univalent universes=20 Quoting the abstract: Thus, homotopy type theory can be used as a formal language for reasoning= =20 internally to (=E2=88=9E, 1)-toposes, just as higher-order logic is used fo= r=20 1-toposes. :)) --=20 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 e= mail to HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout. ------=_Part_2192_836104702.1555416369923 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Mike has released this new preprint on the arXiv:

=

Quoting the abstract:

Thus, homoto= py type theory can be used as a formal language for reasoning internally to (=E2=88=9E, 1)-toposes, just as= higher-order logic is used for 1-toposes.

:))

--
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_2192_836104702.1555416369923-- ------=_Part_2191_1828964353.1555416369923--