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,MAILING_LIST_MULTI,RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.4 Received: (qmail 23266 invoked from network); 27 Sep 2021 10:42:46 -0000 Received: from mail-lf1-x13c.google.com (2a00:1450:4864:20::13c) by inbox.vuxu.org with ESMTPUTF8; 27 Sep 2021 10:42:46 -0000 Received: by mail-lf1-x13c.google.com with SMTP id v19-20020a056512349300b003f72647edb4sf15487432lfr.6 for ; Mon, 27 Sep 2021 03:42:46 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1632739365; cv=pass; d=google.com; s=arc-20160816; b=Yw7mLfErnDZ3ujAe8iQ2S0+ZQoxfpMwmm56UgNwAsvCzkEn/7dCR/qEKLJW64nIYx9 FnjLricaUnuhpYK0eSoD19gtxpPJLvz+YgR6JAEQ7/yV0kJ5sFB4vWT1K1LCQBGZImVB sTcf9RzvkBVsFI6BUAZa4486rnQrDlR6FOH3dAb7QAoc5rwtDvyuW36ZD5+P3axCjXsc wieOtWhVfxzgA8a4tjxpt5GJC5VcATMJoNQ4FS1Bp9+QMPbV0UJjapnUK7L90Jwan6lK F3/ZVRE2WVWMSju6pSjxJMx4TvmjR0d09NqF5VmypyqKJJBBW3rL34Tpvu1hvcAlXavv Q29g== 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:content-transfer-encoding:content-language :mime-version:user-agent:date:message-id:subject:from:to:sender :dkim-signature:dkim-signature; bh=LAsqAz9vjFw/73VYjm6ocGFkw/PgEol1ljXjVLNNvp4=; b=S4FNO88fwtXsDX/Nmdzy3SbiAmmfMPmVG4DlTHENAd+3IPudwh1V8IbtshEB2E3ijt xsAScf2HtXBlcbzdKC/OlwpUIYpQftx4zO+/ADkxcqHuY3n2zw+pfOptV3qEQa36JZkg sdMTGPQl+dsYzqPzwL9n87VJt/ht1rvIVC7FkCSHn68exqP98evOA+kOsBhz73PRFqEL 2dkB/NEIsiB0opBuWpyYZWl5hAzr0j7HdYr4itNQuRSS9i5Z89U7NFgagJKIQNXAOQJX 53rxIO/emQ6Y2ZEWlslK893ymx/Hk/ZBvFZgvxxHs8yipAxgqmxGkTfFFhNVOgFif6Vx aYbg== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20210112 header.b=d3whK0xS; spf=pass (google.com: domain of benedikt.ahrens@gmail.com designates 2a00:1450:4864:20::529 as permitted sender) smtp.mailfrom=benedikt.ahrens@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20210112; h=sender:to:from:subject:message-id:date:user-agent:mime-version :content-language:content-transfer-encoding:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=LAsqAz9vjFw/73VYjm6ocGFkw/PgEol1ljXjVLNNvp4=; b=EYSdwkj/d6KnCN2+aaYr75wmcBpvghISOLBKQs1wmGW3oF5nj0pr+GV0IZewrBpatH lFfUgCNwmOaeHC0FEM9MOmzjWCWvGauBrDaLGEUUUcZHFEZXfUKRKui4IYb2o6GJxLSo PFGz5/HWAPENK73p/AYt1vhB+jpdIe2jhyVeCmUucHrR/cdv4gtFA52HdSCmtt8HdxWA Bfl8DpTf+Yz7ySOdrrrTdWYLOV4L3798FmDarSexVFha7TBF9lUu+MQ+uuVNYu2N3AYN WBXy6wFvMK0F44ajd8cO9Gr8bnbZEiO9mU300lapwjU8j6REWMPeYuf7X1D9BtEsWBm4 m4jw== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20210112; h=to:from:subject:message-id:date:user-agent:mime-version :content-language:content-transfer-encoding:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=LAsqAz9vjFw/73VYjm6ocGFkw/PgEol1ljXjVLNNvp4=; b=YWvZ5BHiJ86DeZpbRv4zIF5/MisfhBIl8S8gwYB+eTsIUiB0aOI5koRH/nhaOnpWKV 0TBQ4EqYFduPbfITekPkDGj7C3IBoUXGjt4LthEqWAJRREtGbfnWn/Edh9qfNfh7Yk4i dEqP82XwU/Nd5kHwGIgTJTVx0lh5wbVoivbm/zZkntiSSBIzpahe9/UtakscPtorTfxM UqFwPTfcJpzOGFbpyI3f+0J91e/3BUj1+7KBhgkDak3obMSd75qtK1rCsUMDXHTEJwH3 T5lqES3f+2Bj0NyJCRyPuwqm4K9ujUfmql61l1NEwLO7jP67Dkmd/X0uCBUVaIefm2An ViuA== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20210112; h=sender:x-gm-message-state:to:from:subject:message-id:date :user-agent:mime-version:content-language:content-transfer-encoding :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=LAsqAz9vjFw/73VYjm6ocGFkw/PgEol1ljXjVLNNvp4=; b=P4fXr559gW4QTjNB/77HsM+nZEErwg+Y4hKUeD7MJ6UlAv7iB+iVimpSoA6ghEOdEh C2tsSLo3AkWdCvl7A+2ll8qtrvTZCBIKOxeGm2ak9vhQnQFhEPjRy1HhY/F7aNy7f6Mg M7FvI4zzgdeDfSX7Fnct263eKhrZTtsElFVLOal8TOa09no9xHoW5l8EhxBqprseWDF8 JIHZ6tbh6m8FtUSkWXYNY7iwoNed4/W+f58nyYqEvckHQz04t241Xz+1x/SIZsnjygOB VtaUZI5RbnI5WVyQT+k0evgXd3lBUOuK7JltB7zvNY48BN98SOndhErQnmjefO/1OhS3 6/JA== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AOAM530Z8PQCV3b9ZonWFkXKOJ/EmGrodJ1hcgT3BiPXKCyuBAKJauGJ 3nkCVS7EvZVqvbNOAf85sfA= X-Google-Smtp-Source: ABdhPJyVKGnlsg/4q9iS/BnUvDLjve55PPEqOzI7XZeXJU/b7ou6T2h5jD9MQ3IOojJuVsjCQ3qLjA== X-Received: by 2002:a05:6512:234d:: with SMTP id p13mr22920808lfu.324.1632739365468; Mon, 27 Sep 2021 03:42:45 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a2e:a304:: with SMTP id l4ls3547206lje.7.gmail; Mon, 27 Sep 2021 03:42:44 -0700 (PDT) X-Received: by 2002:a2e:a688:: with SMTP id q8mr28003476lje.7.1632739364396; Mon, 27 Sep 2021 03:42:44 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1632739364; cv=none; d=google.com; s=arc-20160816; b=WVRW79L33W3jzmlY5UwE6Km/lr+I4aolXVJSWI70opFzRHga7Q5rqqBNTZ8GCmqQ2V 0219OTP48KqoLaG4jDLwks/FgbufCYAUqi5AulCm71pPeccd8Yk58lsOR6wDVwlF7BqV k6ML8t3GBN4HZ8AFs43sOlJzBfEdjlxlH3CUTz9DDWbPjhWlqE4idl9WoiAMHk59UDw1 Yttk0HjtUrW5k/OrE7e2mD4cI2XwIS75j+8RM7mVBCwD3KnbDEp8tPiHrhqHqFcQSIKa DhgTyhHSKScqs6+/H0J6o/5Xw0uwz5D6e2zMCLKsxQKR+LSoonil6U4fC4Du8919J91U UGvQ== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=content-transfer-encoding:content-language:mime-version:user-agent :date:message-id:subject:from:to:dkim-signature; bh=1IeR6/kndVUiZ2Gj51K58XF9fb4MoN1xhI+qV4PGqLA=; b=Ct7nGk+0gTIgiuoyJXLGd74pDYkTNbXZWer0jUErvDUnyz+R89dukAEdh5J9APWqWp Z3EEttkD4kZIjiettQGiMK1jwRsLEEdLXQ+Qxt/+1gK5rxHrmtaEHpR6TnyZEtothcSB 6ml1su3dZP1qgCEue59i/7uGaDBygPNjMKfy+bfxj1gRusjxo0wei0bOsTJgkZ6JJVsh /PDTshIAO8+b5oUvvKQ+LEEa6oskwJUEV+BXWdFzihZvQ8UGsjfmZHHRZy3DsmVsnTGl NmUaAhjg6QUC4IFiVuwPyV6PMxKpap/vNflsYzKtgpxlATfoxrO0nOOEn+SrwA5NSRPM d3Ww== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20210112 header.b=d3whK0xS; spf=pass (google.com: domain of benedikt.ahrens@gmail.com designates 2a00:1450:4864:20::529 as permitted sender) smtp.mailfrom=benedikt.ahrens@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-ed1-x529.google.com (mail-ed1-x529.google.com. [2a00:1450:4864:20::529]) by gmr-mx.google.com with ESMTPS id d15si653193lfj.11.2021.09.27.03.42.44 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Mon, 27 Sep 2021 03:42:44 -0700 (PDT) Received-SPF: pass (google.com: domain of benedikt.ahrens@gmail.com designates 2a00:1450:4864:20::529 as permitted sender) client-ip=2a00:1450:4864:20::529; Received: by mail-ed1-x529.google.com with SMTP id l8so19739248edw.2 for ; Mon, 27 Sep 2021 03:42:44 -0700 (PDT) X-Received: by 2002:a17:906:32d9:: with SMTP id k25mr26364224ejk.290.1632739363873; Mon, 27 Sep 2021 03:42:43 -0700 (PDT) Received: from [192.168.0.101] (5070B429.static.ziggozakelijk.nl. [80.112.180.41]) by smtp.gmail.com with ESMTPSA id ds10sm782327ejc.99.2021.09.27.03.42.43 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Mon, 27 Sep 2021 03:42:43 -0700 (PDT) To: homotopytypetheory@googlegroups.com From: Benedikt Ahrens Subject: [HoTT] Part I of MSCS Special Issue on HoTT/UF published Message-ID: Date: Mon, 27 Sep 2021 12:42:42 +0200 User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:78.0) Gecko/20100101 Thunderbird/78.14.0 MIME-Version: 1.0 Content-Type: text/plain; charset="UTF-8"; format=flowed Content-Language: en-US Content-Transfer-Encoding: quoted-printable X-Original-Sender: benedikt.ahrens@gmail.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20210112 header.b=d3whK0xS; spf=pass (google.com: domain of benedikt.ahrens@gmail.com designates 2a00:1450:4864:20::529 as permitted sender) smtp.mailfrom=benedikt.ahrens@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=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: , Dear All, We are happy to announce that Part I of the MSCS Special Issue on Homotopy Type Theory and Univalent Foundations has formally been published, and is available at=20 https://www.cambridge.org/core/journals/mathematical-structures-in-computer= -science/issue/8405D6FA1D4C76990B57C7E4ADD9A924 The articles making up this volume are listed, and briefly described,=20 below (copied from the preface). We would like to thank the authors for their contribution and the=20 referees for their careful proof-reading and constructive criticism. Part II is currently being prepared and will be formally published soon. The editors Benedikt Ahrens Simon Huber Anders M=C3=B6rtberg Valery Isaev, Indexed type theories Valery Isaev, in his contribution "Indexed type theories", develops a=20 syntactic analog to indexed infinity-categories. These indexed type=20 theories behave to type theory like indexed infinity-categories behave=20 to infinity-categories. Isaev puts forth indexed type theory as a way to employ type-theoretic=20 language in the study of more general infinity-categories than models of=20 Homotopy Type Theory or infinity-topoi. Auke B. Booij, Extensional constructive real analysis via locators In "Extensional constructive real analysis via locators", Auke Booij=20 explores the formulation of constructive real analysis---a notoriously=20 difficult topic---in Univalent Foundations. Booij defines real numbers equipped with a "locator"---additional=20 structure that allows one, for instance, to compute signed-digit=20 representations of such numbers. The paper culminates in a constructively valid intermediate value=20 theorem that determines the root of a function including a locator. Booij has implemented and computer-checked some of his results in the=20 computer proof assistant Coq; the source files are available in a public=20 Git repository. Mart=C3=ADn H=C3=B6tzel Escard=C3=B3, Injective types in univalent mathemat= ics Under which conditions can a function f : X -> D be extended along an=20 embedding X -> Y to a map Y -> D? This question is studied in Mart=C3=ADn H=C3=B6tzel Escard=C3=B3's "Injecti= ve types in=20 univalent mathematics". In particular, Escard=C3=B3 gives two characterizations of the "algebraical= ly=20 injective types", i.e., those types D for which any map X -> D can be=20 extended constructively. Particular care is given to questions of universe levels and the need=20 for propositional resizing. The results described in this paper are fully computer-checked in the=20 Agda computer proof assistant. Cesare Gallozzi, Homotopy type-theoretic interpretations of constructive=20 set theories The interpretation of constructive set theories in type theory is a=20 classic topic, dating back to the pioneering work of Peter Aczel in the=20 late 1970s. Cesare Gallozzi contributes to this line of work in his=20 "Homotopy type-theoretic interpretations of constructive set theories"=20 by also taking homotopical properties into account. To this end, the=20 paper introduces a stratification of models of constructive set theory=20 in type theory by homotopy (or truncation) levels. The models are=20 indexed by two parameters: the homotopy level of the underlying types,=20 and the homotopy level of the equivalence relation which interprets=20 equality in the models. These models are then studied from a=20 proof-theoretic perspective and compared with similar models, in=20 particular, a model of H=C3=A5kon Gylterud is obtained as a special case of= =20 Gallozzi's family of models. --=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. To view this discussion on the web visit https://groups.google.com/d/msgid/= HomotopyTypeTheory/f9a44347-79f7-fc0e-13c7-6c86f5eb8938%40gmail.com.