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.7 required=5.0 tests=DKIM_SIGNED,DKIM_VALID, DKIM_VALID_AU,DKIM_VALID_EF,FREEMAIL_FORGED_FROMDOMAIN,FREEMAIL_FROM, HEADER_FROM_DIFFERENT_DOMAINS,MAILING_LIST_MULTI,RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.2 Received: from mail-pf1-x43f.google.com (mail-pf1-x43f.google.com [IPv6:2607:f8b0:4864:20::43f]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 28ca39fb for ; Mon, 30 Dec 2019 18:05:54 +0000 (UTC) Received: by mail-pf1-x43f.google.com with SMTP id 145sf2216144pfx.19 for ; Mon, 30 Dec 2019 10:05:54 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1577729152; cv=pass; d=google.com; s=arc-20160816; b=QCVFsn4uyWjwb+53eBvT6xGGteKSSVKmu0mXsgjd0EeSKhaZLIyhgHAgNFnvnzSvoK /MaBEmBYr+t0/X1xsYd7hP8si1AiaKOZdlbGql4Y65JPey7Yo+jxhl6N9uZmD5isidQP wlk+lwIrjAGjEzMz2bk9b/x8396LpUeg60Gjpr8t7thebWlc66nonZaoTEJHTFln2hod GTQVgViLwuvY4JJtGaldK0Jb/4xd+hs6qnhS362GhxjKuDOUyRQTCpUId/S1+wx7Q0hc 87dV9WTWMTmHUzv/iWRwHKzUfLS6pDn6yjm+S3SKQjiRHvnSkSrBNJu/HXTuemZLwXk7 mYKw== 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:to:subject :message-id:date:from:mime-version:sender:dkim-signature :dkim-signature; bh=fNGwTF+qeWSQ+oiMPTirnZnVvq8O+X4O2v/uUE5hKg4=; b=tOiOUTseIWKHf3VcM+ByMYaFQhOR9BIlVLwFxUeJDlCtake9WlqrukaL2L37SqMI8/ JV/xyKYutuMC2zgYs+8CeZmZ+EeVXofyBePWRqTZYuedFaC17kePTmgjGyqyqitwRL6U s893EV6uzMLlotwxwzhN7QPdJAtKyvxZk6uurFK8qCDJQF/K1KKZ29kNL39IyFoM3wAF V5FunfHbPxUyW96s2xlQ3R4XUZmiPBNEXeWV9bc8tfhOL2JJ7He+COz6rwnq/yibhN/M foAsBUKU3rdYuk/UH8asmkNqhUCEw9dSiIF35kXsYikqZP0Z51zDabuVtRiB3GSxUmKe HD6g== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=sdkHzQ8N; spf=pass (google.com: domain of b.a.w.spitters@gmail.com designates 2607:f8b0:4864:20::b35 as permitted sender) smtp.mailfrom=b.a.w.spitters@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=20161025; h=sender:mime-version:from:date:message-id:subject:to :content-transfer-encoding:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=fNGwTF+qeWSQ+oiMPTirnZnVvq8O+X4O2v/uUE5hKg4=; b=h/T6iFcNIqMPJxXy5rO9QdCwPQKeZjB33+OoBkSyudFru1K1lIi4wtZFhPGZJxkYJL jmsL5lCI3+NfmW6PVoVsxH7Zx7a8eSRl+B/0NbH1Z1ij3RNOjYGh/qKdCYwmXHL85GLa ABStmKqxd/UYsVfdiqfHcM3C0LRWIo+AOxD+dO9DFcj8P3icx1vUUnANTtm5cTzPW1xL tXOtSg9yPIekwPTzlW5SX3+WdSZHxgbxV+FycN2S/xScLOP85eV7WXqKdZ4PkvaEnzEq wV7mwEEBSwB4xd+PnD6KprBDIXQevKBmyAH6YyxOdF2kcMzdx6f7IcUrV18zQgn+AOh3 ykWA== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version:from:date:message-id:subject:to :content-transfer-encoding:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=fNGwTF+qeWSQ+oiMPTirnZnVvq8O+X4O2v/uUE5hKg4=; b=VDFLUlWn9uGlJZFNGwevaoXynBNGKkxOw/a8dV3uA0UuzZeX7w+RCq/k1l+ctG39Cy DIZ927l6x6l057k4I2wSVRzY97Iix0qhNLgNQvGQEt3hIh6XCmjZMxAirKjRhmZJeG8j lmDlVcsJGnXtPqvjR0nE2gz23udFIuaNdkFUrSG2URKOnxwVro1Q3h6BMMNRmq13b61z EdKwIYDY3J5YYahtJN+wvFiLD2MEr30KtLtxbJzGEJAnf3TZZetkUKUrnbbGmfvI5CpD sXMOPSj7xNJNaadA0ztJfWEgSPWAhFhtyaQXCWJ3jnqrjfFNPdFC8jk3xCdkwEXrSdgY YdhA== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:mime-version:from:date:message-id:subject :to: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=fNGwTF+qeWSQ+oiMPTirnZnVvq8O+X4O2v/uUE5hKg4=; b=VDfv6w5J6wBpURIwq3v6WwYO0yrbfxajXBikCvaXLW/MdQZdNWEQ/fxHEPtsjvejAR TOWchkkDjZINhNP9UjA2JIb3dNK9d3KmaZ5yNsQxZsQ5FHCs3AzTH4cl7L3o/GYZYzeO 53YcFziLuwTtgiPJDjna4a6oTiTk6tCHQ4ZfOC6Vg+2GulvialcKYN9j9awQLx2/u9Um GwurMtivfHWTMfGH1Wg6l85izMkodlbEFvQUIjDPxerNLpDe3tWvVtDR/i/iw+VsJ/xj cZgkxUlZQDd1An04Geq3OV1AA0ZNxJKoobRIpkjrCBt91OeXft5JGbzTrfxAXI2Euy2q M9RQ== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAVoZ87BOtYI4OxrE/ZySYQ5i7YJJ1lLsYZH6M2YuznIF5qCELcG pHVm2C+ok8IX7VnzTtgAjd0= X-Google-Smtp-Source: APXvYqzcz7vIC9pPnCGPAysQGO7wYwpBKBDXt0URWOKTnHdk9EA2dF4VLZg1KVS2RHGlu3RSEUf0xQ== X-Received: by 2002:a63:a54d:: with SMTP id r13mr72917719pgu.138.1577729152727; Mon, 30 Dec 2019 10:05:52 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a17:902:8c8c:: with SMTP id t12ls9396864plo.9.gmail; Mon, 30 Dec 2019 10:05:52 -0800 (PST) X-Received: by 2002:a17:90a:8912:: with SMTP id u18mr422020pjn.64.1577729152322; Mon, 30 Dec 2019 10:05:52 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1577729152; cv=none; d=google.com; s=arc-20160816; b=OOP750LCQsdbPpLkd0L98l+Yh5fRzT+nPfeQcMueLzjIanxRHa/BX97toa5kmCcRnA neVlKGNIw2iYI2maqP92YHU3+lUqE/zyNw1Cha/btjqOa/zQljtda0hmSCSgSgDe/m2X iPK/4t1RzkLD3TwpTsmB+1DwFvRrTRFfVgFiBDxwqToLwpBnecmuQzNeXOP2RGsuuG7h CV/l7fulDji3xz91y3T/5UuBUiFtllf4U3Tw/w28/MEE+ylGMcNP4JZbGf4LmQ2dSlep 9ENrG9g8Mwocb3G5VqxguEFdwYKWcKYDm9Hf7Y2mhGiIj1YVURmoPZ1H3M8hNeITsfJl 5iWw== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=content-transfer-encoding:to:subject:message-id:date:from :mime-version:dkim-signature; bh=QVnJ+qxZcs6tBnYrWJAJjqo7VbvPKWqqoqeHI5WEsyA=; b=zPJzeNv5GWnHNaGCgxz13A3JsbkZBWslrNiAkd+mbC+IeGN8bQjtDU1ujKf3v/V8NI nmfNL9b3kBGdMpg9qvWfmSxsnQ7zQjp3oLCm/Ty3BGKZmUgECUikrdnav4mmUwwlNxDt OmwRDpgLulVlx5Q7L9solEo2U8PGGVuWNlUzmvWgdAX2PT16SVKw5om+XgxUnVSiRhiS hl0dapn55GCd5boASo8iDIiDqXK18LSKIh8sdFbMzc8aLaEtTQRSJ0/xhMM2t4DKKuFr 3JmQ5BhYYlLKOdUzQrAuO74JIxTqc4XQDj9wDuT4j+2WXyoG9PKW6QubhyCzOdOjcK51 YG4w== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=sdkHzQ8N; spf=pass (google.com: domain of b.a.w.spitters@gmail.com designates 2607:f8b0:4864:20::b35 as permitted sender) smtp.mailfrom=b.a.w.spitters@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-yb1-xb35.google.com (mail-yb1-xb35.google.com. [2607:f8b0:4864:20::b35]) by gmr-mx.google.com with ESMTPS id d12si7184pjv.0.2019.12.30.10.05.52 (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Mon, 30 Dec 2019 10:05:52 -0800 (PST) Received-SPF: pass (google.com: domain of b.a.w.spitters@gmail.com designates 2607:f8b0:4864:20::b35 as permitted sender) client-ip=2607:f8b0:4864:20::b35; Received: by mail-yb1-xb35.google.com with SMTP id b145so14382314yba.8; Mon, 30 Dec 2019 10:05:52 -0800 (PST) X-Received: by 2002:a25:5705:: with SMTP id l5mr30867310ybb.349.1577729151358; Mon, 30 Dec 2019 10:05:51 -0800 (PST) MIME-Version: 1.0 From: Bas Spitters Date: Mon, 30 Dec 2019 19:05:40 +0100 Message-ID: Subject: [HoTT] Synthetic topology in Homotopy Type Theory for probabilistic programming To: homotopytypetheory , Constructive News Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable X-Original-Sender: b.a.w.spitters@gmail.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=sdkHzQ8N; spf=pass (google.com: domain of b.a.w.spitters@gmail.com designates 2607:f8b0:4864:20::b35 as permitted sender) smtp.mailfrom=b.a.w.spitters@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: , We have a new paper on the arxiv. Comments, suggestions and questions are very welcome. Synthetic topology in Homotopy Type Theory for probabilistic programming Martin E. Bidlingmaier, Florian Faissole, Bas Spitters The ALEA Coq library formalizes measure theory based on a variant of the Giry monad on the category of sets. This enables the interpretation of a probabilistic programming language with primitives for sampling from discrete distributions. However, continuous distributions have to be discretized because the corresponding measures cannot be defined on all subsets of their carriers. This paper proposes the use of synthetic topology to model continuous distributions for probabilistic computations in type theory. We study the initial =CF=83-frame and the corresponding induced topology on arbitrary sets. Based on these intrinsic topologies we define valuations and lower integrals on sets, and prove versions of the Riesz and Fubini theorems. We then show how the Lebesgue valuation, and hence continuous distributions, can be constructed. --=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/CAOoPQuR4ttw71bPEA%2BxtXZ__Q5kKFGRqgJVgTA%3D2PmLc5%3Dd5L= w%40mail.gmail.com.