From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.129.101.134 with SMTP id z128mr10814998ywb.86.1477423428429; Tue, 25 Oct 2016 12:23:48 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.157.46.13 with SMTP id q13ls3630035otb.20.gmail; Tue, 25 Oct 2016 12:23:47 -0700 (PDT) X-Received: by 10.13.217.209 with SMTP id b200mr12288496ywe.13.1477423427796; Tue, 25 Oct 2016 12:23:47 -0700 (PDT) Return-Path: Received: from mail-qt0-x231.google.com (mail-qt0-x231.google.com. [2607:f8b0:400d:c0d::231]) by gmr-mx.google.com with ESMTPS id x14si1548062vkd.3.2016.10.25.12.23.47 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Tue, 25 Oct 2016 12:23:47 -0700 (PDT) Received-SPF: pass (google.com: domain of b.a.w.s...@gmail.com designates 2607:f8b0:400d:c0d::231 as permitted sender) client-ip=2607:f8b0:400d:c0d::231; Authentication-Results: gmr-mx.google.com; dkim=pass head...@gmail.com; spf=pass (google.com: domain of b.a.w.s...@gmail.com designates 2607:f8b0:400d:c0d::231 as permitted sender) smtp.mailfrom=b.a.w.s...@gmail.com; dmarc=pass (p=NONE dis=NONE) header.from=gmail.com Received: by mail-qt0-x231.google.com with SMTP id q7so144008162qtq.1 for ; Tue, 25 Oct 2016 12:23:47 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=mime-version:from:date:message-id:subject:to; bh=tSruerXgxq/Kra5eLIJ772CswWSkeSvI9pFyXWDBcEw=; b=eymw/BMSlR9KY4rGnW5yXchi4jl5WrOd/mRRyhija85vGxMJOx6CzaVymUGotJPb5h v5TdJiXHyCctpPKeBYIShJ5MjmFUqPuZ0HSAmIU6kgUGYKhWDny0AzCt0E1C9W1Sow4J h3sLCZzhsjbU83TTMP13VMu1Rxld4yabeoLC7/8XWfU1Lvo/4Iy35thox/7nCP49ST6z ptrH9Tk8pin9dWODdjulFc1bXrJwhjpB1G3ycSMEo21n9YiWIq0w7RAlqZs0r5QXxw+Q 21F6wd5T1iBFcKYJ6bP7POhns2eNqcZdOs/DyUuIl9CowepYF+VlHmJAhhBCFWYK1dHu 4lwg== X-Gm-Message-State: ABUngvfUgfK2Jww0551eBeXmGYX4qQpVgri52WGlLGcYKJn9B2K2aE9Tsf9i9jEZyqxxewOZHUg43nQFBq5wLA== X-Received: by 10.237.32.226 with SMTP id 89mr21873521qtb.76.1477423427419; Tue, 25 Oct 2016 12:23:47 -0700 (PDT) MIME-Version: 1.0 Received: by 10.12.136.183 with HTTP; Tue, 25 Oct 2016 12:23:27 -0700 (PDT) From: Bas Spitters Date: Tue, 25 Oct 2016 21:23:27 +0200 Message-ID: Subject: HoTT library To: homotopytypetheory Content-Type: text/plain; charset=UTF-8 We wrote up our formalization work: The HoTT Library: A formalization of homotopy type theory in Coq Andrej Bauer, Jason Gross, Peter LeFanu Lumsdaine, Mike Shulman, Matthieu Sozeau, Bas Spitters https://arxiv.org/abs/1610.04591 We report on the development of the HoTT library, a formalization of homotopy type theory in the Coq proof assistant. It formalizes most of basic homotopy type theory, including univalence, higher inductive types, and significant amounts of synthetic homotopy theory, as well as category theory and modalities. The library has been used as a basis for several independent developments. We discuss the decisions that led to the design of the library, and we comment on the interaction of homotopy type theory with recently introduced features of Coq, such as universe polymorphism and private inductive types.