From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.55.221.156 with SMTP id u28mr4435292qku.11.1516799426900; Wed, 24 Jan 2018 05:10:26 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.237.37.15 with SMTP id v15ls1931038qtc.8.gmail; Wed, 24 Jan 2018 05:10:25 -0800 (PST) X-Received: by 10.200.4.26 with SMTP id v26mr4180447qtg.25.1516799425840; Wed, 24 Jan 2018 05:10:25 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1516799425; cv=none; d=google.com; s=arc-20160816; b=AoQ9rVG7esLmyy9ED9n/qCplPZdWp6K3sHd9BU37B+6uGvtLAvGnTziJE1ttSTRMd/ jgk8m3dn2uZUNsNumVAXWXEjH3Qv1nb0im1fSm8m450nMS0d/AhSxENu0ejWeJr7fm2K sgmAIOFe1s8xZipx5C9YhkdtN9DRSVhCk1qVfJsHyq/IzAstagmKoEWhQFncqGGb4QLu F1NKe+ToWeai/2kkPVI3biK3dIFxOzEjbTX2qtTH6O3KGhegiJuKwYm8UJw3Zri4vIjd ptGtNJ6KmGdJFQSk2S4nZmLs8noFRN7VZvNYJM5DOtAULhe0vOXfGntXu/sd99jPZ8NZ COuw== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=to:subject:message-id:date:from:mime-version:dkim-signature :arc-authentication-results; bh=x3HPAmU0+S3axDiDR+aVosDkmYbX1F/goPU0QSSnmLA=; b=xsaqFyA2YFfKYZGFYsqCFSGez/5vcxiPzeSAQC0vwzXEu2tHcXpbdO3jOin9wdR7t8 1sw4qU2kSE5ueo9OJ6EIZKV8jLkxqg85sVwIDRxps80B86foMOhSxWPpYKIzy0+WElTW 0S16K6Brn6jqn6iMssl+b3gRoGcOq8GPIUU7CqeAsRXUx0Li9Zi3Qyus60KkKizndrzk yzOsgg/rz3r4AyhdNpJTWruPVqeokIMkp83IVn8cuJOQ8981jHZO5mC66b92d2owbyt4 mv8H92r/mFHnUrGWW5TwEpsKCzBSQH2CzMCWghkaT8rRAm61u3b9uBv2XQf5IoRqCh7t EmNg== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=g+vdGbnx; spf=pass (google.com: domain of b.a.w.s...@gmail.com designates 2607:f8b0:400d:c0d::22b 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-qt0-x22b.google.com (mail-qt0-x22b.google.com. [2607:f8b0:400d:c0d::22b]) by gmr-mx.google.com with ESMTPS id a12si202547qtb.0.2018.01.24.05.10.25 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Wed, 24 Jan 2018 05:10:25 -0800 (PST) Received-SPF: pass (google.com: domain of b.a.w.s...@gmail.com designates 2607:f8b0:400d:c0d::22b as permitted sender) client-ip=2607:f8b0:400d:c0d::22b; Authentication-Results: gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=g+vdGbnx; spf=pass (google.com: domain of b.a.w.s...@gmail.com designates 2607:f8b0:400d:c0d::22b 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-qt0-x22b.google.com with SMTP id g14so10065099qti.2 for ; Wed, 24 Jan 2018 05:10:25 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version:from:date:message-id:subject:to; bh=x3HPAmU0+S3axDiDR+aVosDkmYbX1F/goPU0QSSnmLA=; b=g+vdGbnx96E1aYGpJWAfpd+fg4D9MezpMr1nEM6WA1D/IpQOsmAtZt7B8y8a2qh3gq QApW0+NLkTBRSBvDafHph7o2ha+LVpoqC/JdBTNmCpbVL1M4znpqqQDY/Pvmpx6HFeXx Drezaoxh4kYFa1ecOrLJWxoaThoB7DSk7rXiILvMu2mf31BO1cUn2b8v8dhVECsfIt2h kPd6EzLeFMSx4wGvz+eBsH2V7WW5ZG4ggMBwu2NoRdvcpXTrSsrwjmlnlMU+OGa5Xmqu ydYC/qCOVQpd5nT8sWscNNxMzM64yc11qvUa+KkaezOKaIEn0Tm0xXkxmdfILKNg9+MC FCnw== X-Gm-Message-State: AKwxytd3bqiefNp5aUtozWRGWF6l/ET/4fVPbGAOWZ9Q9aOpI0t0aMtp rAVReAB3kUrC/br5btqXLYvbQcpMMtzQzWfIjT5oikFQ X-Received: by 10.200.57.228 with SMTP id v91mr9643528qte.121.1516799425238; Wed, 24 Jan 2018 05:10:25 -0800 (PST) MIME-Version: 1.0 Received: by 10.12.149.188 with HTTP; Wed, 24 Jan 2018 05:10:04 -0800 (PST) From: Bas Spitters Date: Wed, 24 Jan 2018 14:10:04 +0100 Message-ID: Subject: Internal Universes in Models of Homotopy Type Theory To: homotopytypetheory Content-Type: text/plain; charset="UTF-8" Our paper has just appeared on the arxiv: Internal Universes in Models of Homotopy Type Theory http://arxiv.org/abs/1801.07664 Dan, Ian, Andy, Bas --- Internal Universes in Models of Homotopy Type Theory Authors: Daniel R. Licata, Ian Orton, Andrew M. Pitts and Bas Spitters We show that universes of fibrations in various models of homotopy type theory have an essentially global character: they cannot be described in the internal language of the presheaf topos from which the model is constructed. We get around this problem by extending the internal language with a modal operator for expressing properties of global elements. In this setting we show how to construct a universe that classifies the Cohen-Coquand-Huber-M\"ortberg (CCHM) notion of fibration from their cubical sets model, starting from the assumption that the interval is tiny - a property that the interval in cubical sets does indeed have. This leads to a completely internal development of models of homotopy type theory within what we call crisp type theory.