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.9 required=5.0 tests=DKIM_SIGNED,DKIM_VALID, DKIM_VALID_AU,DKIM_VALID_EF,FREEMAIL_FORGED_FROMDOMAIN,FREEMAIL_FROM, HEADER_FROM_DIFFERENT_DOMAINS,HTML_MESSAGE,MAILING_LIST_MULTI, RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.2 Received: from mail-lj1-x23d.google.com (mail-lj1-x23d.google.com [IPv6:2a00:1450:4864:20::23d]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id d1b5ab1d for ; Thu, 8 Aug 2019 18:33:07 +0000 (UTC) Received: by mail-lj1-x23d.google.com with SMTP id 17sf18944437ljc.20 for ; Thu, 08 Aug 2019 11:33:07 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1565289186; cv=pass; d=google.com; s=arc-20160816; b=aA67RRG/KEOWSYe6MmilkECdZ8dVWR3Nd/yoBVy/v9igq3uPPOvPz7ZkSgmQQfqVtk 415gHSgtvw+u4h03cWVsOXbLqAmlQU0tVL1+4wI9U955VPqGroI5Z4tBQ27ZKxEUSGpI pO9TisNneFC13+iVnSTG10ftj2F5L5LSk8xltlygFmVu07YaU2RUyaiJxNVYBFwM7rid mv1Mplg9sEnjVnAPlsnEo2koTM+DhPUHosw65DJFFMusWZ9YwSqQImqtx9ePO7nYqinM gyzmh2d8+fAaAePTkm8mYJpVe2VysBzxi2uBzOqVIbJEp6M/MEbO+WEj7rTlcdMpz7e5 zXuQ== 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:to:subject:message-id:date:from :mime-version:sender:dkim-signature:dkim-signature; bh=kGDQ0P27uvIX0Yf/jXzT3yYx+bVMmGyLfzF2TIxnq/Y=; b=Yx4w7TWcHWD2E0YtRS39gGSmQeFP8qPziw6X7hFQL2f54/urIFs5nrlDZh6HfkiYvO BLoghvcTzQLC2sv9bsugXQbBbzdp1q4VCgzzwDZNqMjj/bg+felXTLp40kaPTVFX1rx6 2RUhyfAVE5C14uKaFXgm9WU9p/Q9aEdcl+MbW6AYWNCXAO/NSLHQsd8IRAd6j+6lbtJ4 bZ4o4prvc3MkcqNg6IVvEHFxSxiTmAs9fCHvGDZyqcOf0xju4eNA1ac0eZVkFkWVPLV3 m9CeA3YvfYbXDnskrxzevrjDCY5j+Z5tydONd9CMsSiteZVYqoBgyO1lyFK3tDxu2rHZ hG8Q== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=lxHDFokb; spf=pass (google.com: domain of intoverflow@gmail.com designates 2a00:1450:4864:20::233 as permitted sender) smtp.mailfrom=intoverflow@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 :x-original-sender:x-original-authentication-results:precedence :mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=kGDQ0P27uvIX0Yf/jXzT3yYx+bVMmGyLfzF2TIxnq/Y=; b=fvNGbXuj96ejrWtps4ZYExoiSgmdCLykMvU8Uqs+y6lAad+cQcxv/sW27/zBINpQ3y viobaReq6kaxG/m/5J/dmKMMDCnTGmIDJBu3BjWig3ZsxmFyu7AKBP50xrEpYBfuABQR W3r1JjxZr8NmThp8a2koTfwD/bwoVYzqqXRZHsB22NDCo9t5lKVs2NqhanOvyvbACaDA WD3go/6/JrjDNMJPGaR3BvSPZSn/oast0J3xBHU6g027IvL4UEsbNnz7268yNdjZXP4W I5MqemwZt/MtF+1g0o8H/pCFyAmAiNp47Qeo/c2+BdDZwT77MBPl81ew8f+92NPqyJ3E 29ew== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version:from:date:message-id:subject:to:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=kGDQ0P27uvIX0Yf/jXzT3yYx+bVMmGyLfzF2TIxnq/Y=; b=V8+wyCyVNxsOvk+oV2HDQQyCLZ5ORHJTG1bDKKdAupxX8BfsYtb7tPw9dm9MJISBrE to4Nre+ku7biLzsyxrAlx1RNBTETNeR91XDxezIRmSzNnNrctt0Ze87dWTwnB6BaW+uL V8m7Kl8wauqDws9J/RcWm91AhAbje1IviE7oSeewY1nuxrXB6TnAONjuOSZf+SBCzrFr TUHAtB0pZjx43Crj68BdvwlEzADPmsl47zeZEr91YpQN0yJZUJqw7+OE2k0trPadxEkU Gmm83ZeF1S/pJEu8RljaYhL4LEz037519FdC+1y2rf/ZsHKE9oRvAYH6lk0EKLOkapuW 039g== 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: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=kGDQ0P27uvIX0Yf/jXzT3yYx+bVMmGyLfzF2TIxnq/Y=; b=nAEzF2i4Rub6mv+sJZ6DAPQjbCMZNIpLlL9sN6REFs6h55mypkO8p2NhX5huoJG3uJ S3pBvq8hvsveVy6vKG5x2ukzWSb2jAJCh1FgUbRn/hANp0Szt0w6CIDMiQdJ3T9bg6TH 9EZvndORK7SKyJb3aI1vqzWteYQQ1XzDuJjFykA2tLWaagdb8/y4fY99finbFipfTC86 T5a7OlzumxU7NFGLpC5Fuuq8qK1rvV2VQpqBjgNXw4rlSzAlOJxelRAyFK+pWniT9f+n gQhCet6UAWdWPd1bUrStta//JY3Iz/n6+19196y60Jk/a0IFqRpu4MAfS++EsBkVXFHP WhOg== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAXlHilaMeqG+gqI1SCa/RmN4VuSJSKwRx/a0pSnbFnStpoEkh8n dvuROWOOAsWCNZGF7HwV9dE= X-Google-Smtp-Source: APXvYqx1XtUxz6UDPNSaBpeI3cDTu8g712htbcwiu9uUArrOE/36/KJhmTeJ1kvLNRQDbvMhYUfppw== X-Received: by 2002:ac2:4824:: with SMTP id 4mr1710916lft.161.1565289186605; Thu, 08 Aug 2019 11:33:06 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a2e:8917:: with SMTP id d23ls10780983lji.14.gmail; Thu, 08 Aug 2019 11:33:06 -0700 (PDT) X-Received: by 2002:a05:651c:c6:: with SMTP id 6mr9228716ljr.127.1565289186095; Thu, 08 Aug 2019 11:33:06 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1565289186; cv=none; d=google.com; s=arc-20160816; b=i06Sf3wsj1SfUnUwwbyrl12ejPnPBRVwg0dxQDj2xAzTlbVvxsu3+LaHq9aGVWIfGa u5njU1NK90Xh8rLL563uAxFOTCyWt79yflh9URzodXb81etMn4n3MX7aSG8gvNaWjEzl EFukUvLkII/8slebg4jqMs7U3ZY+ewUh8dOmpokm3bJtaboGUXQxq+JnscWt5i5kyOL/ Kwpu2smwH6o7vboH8ZvfnWewWwnkxLXMU1BLJanetvMYuCAEeTCLz7Iua/Nw3VFjVUhG nJEwN8IaABXbLDIx9H+UazT/85+7axEWyHsYWBgvnKfoI7Z57lxZFQ3gVDOK0lNr69Wm C4vw== 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; bh=fX7ImR4A1I0CEsBA16AZzzSTYSDl5p7qyasvw3YgHV0=; b=xIct5Y7z59aR/hmXHVX5SW5oY17F2kh29waEqBV2f+qky/S1Tax4bbAgyjF/uUBef3 w6HSxKXkKvNg4zbThsFDcsC2fuEvTtN3T35IOPEvWYM/1nGdW6hMO44e9HFNuYw6ONr3 OpFgbXvMLBTLFFZLyemU542MCVy01MU/E6iByiRh6kt5M5Zr+DMsUqOWPTlvFI2d7CFb oFYeNHmOQzTSpnfTArLBYc1v10olOseWLFIkKFvbBDXMkF0LwLN6Ncj1imR9HZUUamV+ XIP82lGGNatxTZM9udfOIizF3SUHeBpnVfrTAMMeS0BGoIKNjrB1jC2kypbQtqmhX9j3 IdtQ== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=lxHDFokb; spf=pass (google.com: domain of intoverflow@gmail.com designates 2a00:1450:4864:20::233 as permitted sender) smtp.mailfrom=intoverflow@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-lj1-x233.google.com (mail-lj1-x233.google.com. [2a00:1450:4864:20::233]) by gmr-mx.google.com with ESMTPS id f26si4612134lfp.5.2019.08.08.11.33.06 for (version=TLS1_3 cipher=AEAD-AES128-GCM-SHA256 bits=128/128); Thu, 08 Aug 2019 11:33:06 -0700 (PDT) Received-SPF: pass (google.com: domain of intoverflow@gmail.com designates 2a00:1450:4864:20::233 as permitted sender) client-ip=2a00:1450:4864:20::233; Received: by mail-lj1-x233.google.com with SMTP id v18so89744132ljh.6 for ; Thu, 08 Aug 2019 11:33:06 -0700 (PDT) X-Received: by 2002:a2e:9e81:: with SMTP id f1mr9160216ljk.29.1565289185654; Thu, 08 Aug 2019 11:33:05 -0700 (PDT) MIME-Version: 1.0 From: Timothy Carstens Date: Thu, 8 Aug 2019 11:32:54 -0700 Message-ID: Subject: [HoTT] (Beginner's question) Uses of HITs beyond homotopy theory To: Homotopy Type Theory Content-Type: multipart/alternative; boundary="000000000000e1bd43058f9f49a4" X-Original-Sender: intoverflow@gmail.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=lxHDFokb; spf=pass (google.com: domain of intoverflow@gmail.com designates 2a00:1450:4864:20::233 as permitted sender) smtp.mailfrom=intoverflow@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: , --000000000000e1bd43058f9f49a4 Content-Type: text/plain; charset="UTF-8" Sorry for the broad & naive question. I'm a geometer by training but have been working in compsci for most of my career (with lots of time spent in Coq verifying programs). I've got a naive question that I hope isn't too inappropriate for this list: can anyone suggest some papers that show applications of HITs? I'm embarrassed to admit it, but I don't know any applications outside of synthetic homotopy theory and higher categories. Perhaps categorical semantics? But even still I'm not personally aware of any applied results from that domain (contrast with operational semantics; but I am extremely ignorant, so please correct me!) All my best and apologies in advance if this is off-topic for this list, -t -- 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. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAJGt_zG%2B04Rfbs_py%3DPYkubbwzeYb0TRhhfek-RT663uVUo%3D-A%40mail.gmail.com. --000000000000e1bd43058f9f49a4 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Sorry for the broad & naive question. I'm a g= eometer by training but have been working in compsci for most of my career = (with lots of time spent in Coq verifying programs).

I've got a naive question that I hope isn't too inappropriate fo= r this list: can anyone suggest some papers that show applications of HITs?= I'm embarrassed to admit it, but I don't know any applications out= side of synthetic homotopy theory and higher categories.

Perhaps categorical semantics? But even still I'm not personally= aware of any applied results from that domain (contrast with operational s= emantics; but I am extremely ignorant, so please correct me!)

All my best and apologies in advance if this is off-topic f= or this list,
-t

--
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.
To view this discussion on the web visit https= ://groups.google.com/d/msgid/HomotopyTypeTheory/CAJGt_zG%2B04Rfbs_py%3DPYku= bbwzeYb0TRhhfek-RT663uVUo%3D-A%40mail.gmail.com.
--000000000000e1bd43058f9f49a4--