From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.99.55.22 with SMTP id e22mr5639715pga.58.1498636984766; Wed, 28 Jun 2017 01:03:04 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.36.211.144 with SMTP id n138ls2008617itg.11.gmail; Wed, 28 Jun 2017 01:03:03 -0700 (PDT) X-Received: by 10.129.87.145 with SMTP id l139mr5677212ywb.88.1498636983835; Wed, 28 Jun 2017 01:03:03 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1498636983; cv=none; d=google.com; s=arc-20160816; b=SGdS7tDM431Hh8G6BlyV8NFRp5ToZ5BQuS/JO0ca2GO1Hvdoj0PcAdz2RdQ3HC/J0Q GtAHt1zp7cfdev15RVpPrw2ziUG+6GLijY1BMwkWxS7sQ/N3qPI5u+bnpp9fWu4ZR8Nf jSUVOLMlwDTWxxV7u4HmidzPhbfM4Xb1eURZ6k0i+hzbnBeeRqdsVy2pVTjhMrilMdIX HRe7jsIGLwA71L7mhiNJBVLMYGOBmLKdODUCxAOo+cslLScJ78xBWDkp17fykNsTl5Z4 MAg3Jwii/SimNuIgqtzP7czRlhn67oFhZyS11NfJxiTthbepkjFWEq9zpDCPLFtbYsAd yetg== 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:arc-authentication-results; bh=PYBRWj+rXcmRRUi3saZLGapgtj9ZW9Sk68XFM3tzfKM=; b=BD+sKFOyhW+J+yJ1sauzMSSm3x7vmGLG4QdTwbLHtxyRn1v63KUnNnsZ3eBCw9b/pb 5LBN8uc7MAy1kmqzUDQrSVMBBdV1zRa5CMkfLgFDKyNqB0apu2b8h1up5GF7ghbfnRSz /e/m25fsal0sAh42m0bvbiTHM9Ey86Nfy8EOBpUkp033EJhZ+6r8Xfynhtx96J3fl9op gUJ1Lt3JiKZ8jAg2rq4YdBerXBfMjCep7ikJSSHtbZF9o0RSVKdHKhEFu2LfyBWmokfK d6jMuBA0DdFpRtklqKfmQbL+di15wKlxmIZ+Upz+0koIkEHO82V3DWTO36pNLlBxwHXb equg== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@gmail.com header.b=Vt4OgXb3; spf=pass (google.com: domain of b.a.w.s...@gmail.com designates 2607:f8b0:400c:c08::229 as permitted sender) smtp.mailfrom=b.a.w.s...@gmail.com; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=gmail.com Return-Path: Received: from mail-ua0-x229.google.com (mail-ua0-x229.google.com. [2607:f8b0:400c:c08::229]) by gmr-mx.google.com with ESMTPS id b77si70326vke.3.2017.06.28.01.03.03 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Wed, 28 Jun 2017 01:03:03 -0700 (PDT) Received-SPF: pass (google.com: domain of b.a.w.s...@gmail.com designates 2607:f8b0:400c:c08::229 as permitted sender) client-ip=2607:f8b0:400c:c08::229; Authentication-Results: gmr-mx.google.com; dkim=pass head...@gmail.com header.b=Vt4OgXb3; spf=pass (google.com: domain of b.a.w.s...@gmail.com designates 2607:f8b0:400c:c08::229 as permitted sender) smtp.mailfrom=b.a.w.s...@gmail.com; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=gmail.com Received: by mail-ua0-x229.google.com with SMTP id w19so12048921uac.0 for ; Wed, 28 Jun 2017 01:03:03 -0700 (PDT) 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; bh=PYBRWj+rXcmRRUi3saZLGapgtj9ZW9Sk68XFM3tzfKM=; b=Vt4OgXb3M8GPGZX152LE4opxWPmasvhf37+AeNFWtGE5jwaW1mE08N6E40Nd0e7moV f55houtUJEKZ08lfFictLK8q7DOwO9ZoGwYYUsCgwuLLZqyMvgoS4z4TA1/PFa5qjS4W nEp2Rm0K2kTw1NiyaclxCQCZhTsSdVUEHAPbcZ3eb9d22xRc3ny7AVmKYk6uyPcTdVx6 l1oUw+t86c+NVQIQ9D6jtgl0QWqa43+QkrqzevxN8Huimt89/EFx4XzIeGDHV//kRFYG oFljNvLUDvUbbN886BxD/ucaStfWjHwjMvTosnp2LW6018eBfLNUMPNjyiggLKBgou6s TB3A== X-Gm-Message-State: AKS2vOxfCQttrfVPQQU+a1+wdDYJ4M2t+0CmTLcqR5X7YDLTBcw3D331 N8j8soVkf1kNr5q3DUNjJGK4vidH/GOd0Ms= X-Received: by 10.159.48.214 with SMTP id k22mr5538275uab.31.1498636983536; Wed, 28 Jun 2017 01:03:03 -0700 (PDT) MIME-Version: 1.0 Received: by 10.103.133.69 with HTTP; Wed, 28 Jun 2017 01:02:43 -0700 (PDT) From: Bas Spitters Date: Wed, 28 Jun 2017 10:02:43 +0200 Message-ID: Subject: Modalities in homotopy type theory To: homotopytypetheory Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable For your enjoyment: Modalities in homotopy type theory Egbert Rijke, Michael Shulman, Bas Spitters Univalent homotopy type theory (HoTT) may be seen as a language for the category of =E2=88=9E-groupoids. It is being developed as a new foundat= ion for mathematics and as an internal language for (elementary) higher toposes. We develop the theory of factorization systems, reflective subuniverses, and modalities in homotopy type theory, including their construction using a "localization" higher inductive type. This produces in particular the (n-connected, n-truncated) factorization system as well as internal presentations of subtoposes, through lex modalities. We also develop the semantics of these constructions. https://arxiv.org/abs/1706.07526