From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: homotopytypetheory+bncBCALZ6FR2MJRBWFAY7MQKGQEHOQ6X2A@googlegroups.com X-Spam-Checker-Version: SpamAssassin 3.4.1 (2015-04-28) on inbox.vuxu.org X-Spam-Level: X-Spam-Status: No, score=0.7 required=5.0 tests=DKIM_SIGNED,DKIM_VALID, FORGED_HOTMAIL_RCVD2,FREEMAIL_FORGED_FROMDOMAIN,FREEMAIL_FROM, HEADER_FROM_DIFFERENT_DOMAINS,HTML_MESSAGE,MAILING_LIST_MULTI, RCVD_IN_DNSWL_NONE autolearn=no autolearn_force=no version=3.4.1 Received: from mail-ot0-x23d.google.com (mail-ot0-x23d.google.com [IPv6:2607:f8b0:4003:c0f::23d]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 35ca56db for ; Tue, 26 Jun 2018 05:34:18 +0000 (UTC) Received: by mail-ot0-x23d.google.com with SMTP id a1-v6sf10683462oti.8 for ; Mon, 25 Jun 2018 22:34:18 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:date:from:to:message-id:subject:mime-version :x-original-sender:precedence:mailing-list:list-id:list-post :list-help:list-archive:list-unsubscribe; bh=pkHkeJKwjSgwQqzlq4etvkk9YR+6wqgJbwN4w8oNCp0=; b=tL3QjbwpV7RvmVe1srBwfqXgdQm3qibThCCDpc7nf7HYobgFWX2sKVBz8zk12Q6GvG 2PEZMNo8P0+QLqC4JO5D3mlZ7lnxukWDhipuA6/vSdBISgUR/ZgOnHvyeghkKNyEu1s3 tMZEyVXFBLwzjg+UvaKCJXYZ38uOulF0qreyMAnwQvCbhXWkFGJmLWp1U2YkspO3xhYO l/wnpDN1QIhHggztr78VsXB6JJQvOQdyICBRXvUy8Btzu/ALX/unMW5UacGtpxFa5vRM NqN23JDW7h8ak7j2Spjt0tA1t/nfU153Smdfm9iDfgd15oH2mS2FqDJwrM6dg6QEvqLf BMgA== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:date:from:to:message-id:subject :mime-version:x-original-sender:precedence:mailing-list:list-id :x-spam-checked-in-group:list-post:list-help:list-archive :list-unsubscribe; bh=pkHkeJKwjSgwQqzlq4etvkk9YR+6wqgJbwN4w8oNCp0=; b=Ri+zDi3XoHfj6ChhH+XTWD83jXePSpYTLp+2hr7XPNTaSNEM4glo2xAgPy6j99l0ZS y1VHPvFITMIxgiEso/A3gRHzhBxH4GY4RL4sZkJUyjJlMEw1C/CPB3h/8HFg9WRnA2rY C66zGdGg+urw9O/WV3nSy44zcCpmQ1LoFsQPTlcpHNjAbPjNCd+fxTFzu3Zjx9HTbxo1 HBm/7JAxp27mf0x7n8SX44llyA519T7EBFA3PViR0vDGRYJ6HRPkwj4UtZ0na4+VGUzw Q4fdc7c0X15+1UQD8QVcw5xtPCq+XGoinzAMQ6kyGPIAPlNDZuvrkJzR3xM76xWuggqb mRtw== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APt69E0gikbQ1ZDVDFTrVrF7aNPzjKnOOoYFyHTzSHRezOGJwD4ymHEV BQgxQDNi5UnxKZUuCCXEeNk= X-Google-Smtp-Source: AAOMgpca8NkCCpPCyw2kO2zzRfVgBEwKAXI5LzCcuIDXBk9xUSSfPzQ5bC9Z0aIzdSTb3KTdS/slGg== X-Received: by 2002:aca:ed52:: with SMTP id l79-v6mr10313oih.4.1529991256957; Mon, 25 Jun 2018 22:34:16 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:aca:908:: with SMTP id 8-v6ls335159oij.20.gmail; Mon, 25 Jun 2018 22:34:16 -0700 (PDT) X-Received: by 2002:aca:1a18:: with SMTP id a24-v6mr7580oia.5.1529991256544; Mon, 25 Jun 2018 22:34:16 -0700 (PDT) Date: Mon, 25 Jun 2018 22:34:16 -0700 (PDT) From: Bruno Bentzen To: Homotopy Type Theory Message-Id: <7a29a201-7bd4-4a33-b12a-80c816cb1691@googlegroups.com> Subject: [HoTT] Preprint - Cubical informal type theory: the higher groupoid structure MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_33385_498462338.1529991256098" X-Original-Sender: b.bentzen@hotmail.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: , ------=_Part_33385_498462338.1529991256098 Content-Type: multipart/alternative; boundary="----=_Part_33386_1896970809.1529991256098" ------=_Part_33386_1896970809.1529991256098 Content-Type: text/plain; charset="UTF-8" Dear All, I have recently posted my new preprint on arxiv whose link is attached in the following. https://arxiv.org/abs/1806.08490 Title: Cubical informal type theory: the higher groupoid structure Abstract: Following a project of developing conventions and notations for informal type theory carried out in the homotopy type theory book for a framework built out of an augmentation of constructive type theory with axioms governing higher-dimensional constructions via Voevodsky's univalance axiom and higher-inductive types, this paper proposes a way of doing informal type theory with a cubical type theory as the underlying foundation instead. To that end, we adopt a cubical type theory recently proposed by Angiuli, Hou (Favonia) and Harper, a framework with a cumulative hierarchy of univalent Kan universes, full univalence and instances of higher-inductive types. In the present paper we confine ourselves to some elementary theorems concerning the higher groupoid structure of types. Any corrections, comments and suggestions are most welcome and appreciated. Best, Bruno -- Bruno Bentzen https://sites.google.com/site/bbentzena/ -- 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 email to HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout. ------=_Part_33386_1896970809.1529991256098 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Dear All,

I have recently po= sted my new preprint on arxiv whose link is attached in the following.


Title: Cubical informa= l type theory: the higher groupoid structure

Abstr= act: Following a project of developing conventions and notations for inform= al type theory carried out in the homotopy type theory book for a framework= built out of an augmentation of constructive type theory with axioms gover= ning higher-dimensional constructions via Voevodsky's univalance axiom = and higher-inductive types, this paper proposes a way of doing informal typ= e theory with a cubical type theory as the underlying foundation instead. T= o that end, we adopt a cubical type theory recently proposed by Angiuli, Ho= u (Favonia) and Harper, a framework with a cumulative hierarchy of univalen= t Kan universes, full univalence and instances of higher-inductive types. I= n the present paper we confine ourselves to some elementary theorems concer= ning the higher groupoid structure of types.

Any c= orrections, comments and suggestions are most welcome and appreciated.

Best,
Bruno

--
You received this message because you are subscribed to the Google Groups &= quot;Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an e= mail to = HomotopyTypeTheory+unsubscribe@googlegroups.com.
For more options, visit http= s://groups.google.com/d/optout.
------=_Part_33386_1896970809.1529991256098-- ------=_Part_33385_498462338.1529991256098--