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-vs1-xe38.google.com (mail-vs1-xe38.google.com [IPv6:2607:f8b0:4864:20::e38]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 6e457ec8 for ; Thu, 8 Aug 2019 20:18:14 +0000 (UTC) Received: by mail-vs1-xe38.google.com with SMTP id q9sf363440vsj.0 for ; Thu, 08 Aug 2019 13:18:14 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1565295493; cv=pass; d=google.com; s=arc-20160816; b=VVWzsItq98YeX3w1h7/MnzN4jATIX/+xaXFe5Dt0oXeKSS4++BFEPcUj6UzCckHMR9 xgk3hJxaMl3sy0KtKK8yjP7wO3gifBZIgiEAs66hdhd1XTWjKjIoTsukMsKdENDuHZ2p EgS540+sUkomnlVeLNEBCAbAbOoFpnUCEFa30uAU4mvelPraVcLgAzmUN5xAWgSqyMgD 7mBHEZeLCAmz4OjiM7MAhd1Mgnk75WVy66d3viXyrrdmvruSEomTcn3Kg39iJfycsPsX ny+A8FeokTWoYq05krqpZQaWswQk8f1GUkRprlhiJ+/xembdxS/tIRZkQ2zuTAtl0l26 JXpA== 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:references:to:cc:in-reply-to:date:subject :mime-version:message-id:from:sender:dkim-signature:dkim-signature; bh=68OJEk3oJWKGr09BpNjcCkpKPONNWAuNoA0NiK2I6us=; b=WojVvBjyCWrFkD9OLZYJRdnJrl2JUzTbyeOWNd9LBW/VR2Sc1EBd+b7vmzXM5rkYBH deVE79+sVJglAkv29u2RxCsb+QMNaL03Efz5sbsdqT5WSCNmHjkGNZFhifpG+pTtfSei mOGBmt8oWaCpIrb64Ok8xd4tE9ucUj2uogHgKVqxIttfDc9v3b0fqQHMJthmLwtH+Jzd UaqQceXcnozJOKqCi6aYB+lttP7LoibozAtrvrr8XpC2q7wtIK1b6/XWY8nGWJ90tD7q LG0FKk4P+tzdkexL5hymlYMdtwIi+DDfFvl2UUKu76TG197AIR7x1iHPp8raxGPH7TIu hP2Q== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=KiUaAkV1; spf=pass (google.com: domain of steveawodey@gmail.com designates 2607:f8b0:4864:20::72f as permitted sender) smtp.mailfrom=steveawodey@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:from:message-id:mime-version:subject:date:in-reply-to:cc:to :references:x-original-sender:x-original-authentication-results :precedence:mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=68OJEk3oJWKGr09BpNjcCkpKPONNWAuNoA0NiK2I6us=; b=dYTbx1ThI7fG9e6dvegdi9tFDBej8ensms0CTDaKLzGe3+zgkqRtPKJHd3NUbniO3D oqlh4sLTWmWVVruTgq89bf1fZM19QMYHs26s2am+v57Xxu0ASRgVDsr4pmVnaWeN2Qsd Vf8+kml4iP+dClBb9eYJDkeuas6WEKNKaFREhYYOIQ6KtXK1ruklzAW8Sk986gVBW0Iq jEA2ht5cuVKfAxJDIbdXi8sHqnbbBaL3ujmWaxVCn0ri1qqeeW0omzX3gISGL4bNAIM6 D7rnp53oplTvi4FikD4eLs+mbinUtDny5drjf1d4x5MFiYuNa4mooYc4ZoMgv42Pdr7J WItw== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=from:message-id:mime-version:subject:date:in-reply-to:cc:to :references:x-original-sender:x-original-authentication-results :precedence:mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=68OJEk3oJWKGr09BpNjcCkpKPONNWAuNoA0NiK2I6us=; b=lhOH92t0AKQ6ftJeaNGNViWF+MObhteMFLp0XhfJgEjSV1uFc3XMtRRXIakiUUGue2 1CQ/hPvnE0i9tKcigTm4wEjciqpMFxFKJVs4o3bkcRM9ZPyQLAyVlBkpL6Ol8wgGcCAN rXd35YywZDgdpFgrFk2TukmcVJqHG61i7VTclxV1CAkc+Ob3lKYVhFvDS6HPIIraWzft Rw0GsdExl/826bo+LI5X3Fi0D6aKYA2jJ9w5EvW+Hd054Zz9t+mw3iQk8RB8RPVy9Bhl SqqPKTOHlRrSG5WTJ+JtW5qk35LHZuufCMezMSyUdeEYLWIwCt0+B8yvo+v3Dbvh314j Slgw== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:from:message-id:mime-version:subject:date :in-reply-to:cc:to:references: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=68OJEk3oJWKGr09BpNjcCkpKPONNWAuNoA0NiK2I6us=; b=kJtJN64Ah3bKGTVRTRdzTXhJlEpSQDCsEw9BxAVN37RwCC3f+w+clApbZ7qjZEQYLP Qs37dvZwWEINZ/cQZQiona2TUFJE1Ft8i8kiodl/3KLGvQwOmQiqvsOauB5BA8wJOlKR PRwgmsfVsCrs7jmAjUFcOsDc9E508DsP32ZKY7JZJ5iIfjJR/4s7fdcJNM8vUFbIRiQ4 twpP6koQQvsnStWN4zg1To1YP7L6H5AWS6kNA1S/Mh1zztt/no8U2v4JYzHZ/dlPkRgb zv8cWMsQ1FTCe+sSdEfY7MNEU6asiYU4Nk1D2oVzLNROIQtUIZn27d3qLw4Zs6bgchnF TMzA== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAViCaDmVppZgo7XkYZDvc6IYhWE1Z9a6FciIIrCpOx8nwJ2fjIk uo/4ZXj+cKEaVG4ZwhA1fWk= X-Google-Smtp-Source: APXvYqx32doTKFYqGva0OfEmfYVot6DACVCgbqthnrH52S4zwiBqTfT+TQcM/iIlik2jNePmNbeAGg== X-Received: by 2002:a9f:21e7:: with SMTP id 94mr10966064uac.137.1565295493114; Thu, 08 Aug 2019 13:18:13 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a67:d712:: with SMTP id p18ls11954147vsj.14.gmail; Thu, 08 Aug 2019 13:18:12 -0700 (PDT) X-Received: by 2002:a67:1e44:: with SMTP id e65mr11681184vse.45.1565295492877; Thu, 08 Aug 2019 13:18:12 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1565295492; cv=none; d=google.com; s=arc-20160816; b=E4/w6FcUanLbxBlcyhiJjvcJDflY+tzXozMeqLH3DwI+C/I28NB/GP+7uHqgIny2GQ xgpPDqbrbKbGLWYl5VZYOO3Rt4jtgcf6o/bGStZQTDSmxcjxHAOnayuSnNN4di+2pPAL 3VVguxv49UHhslsbr/6IJfgc98AoyT7f5ufDan+kf7cwo/1SqJJldtiK2OP7sIlKLkHl lmtKoM0HWff1IRIdZ46eHDuiYqHDphpfL3tqKOe5C3E0H0VR8zol6NgNDbLO+d5UHydB SEEBiovFfw3h0TWETR5Veb6bL43AARID2LThA8k0/W7jU1/nKF8dQRQfehcVyVsQy2A/ W75w== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=references:to:cc:in-reply-to:date:subject:mime-version:message-id :from:dkim-signature; bh=gWBWw357m/7+/0XwC/ztXqhTSSz0k8EgeoihDH0f/qk=; b=mK4kc6rprcZCQ/kEFjb+EauHCnCVt+xViPlMb+Q4JW9+Aku1k/NTZaiVmEKnw39LLf J/73zNM80Xycy/T0IXpoFD+vwaJ2LtvdMXo2cjXxIJ1utXqnUkW5hwWMaxIrRQ7k3TUP tU3XJ7uoJgUarwIeWzuh5PzRRRYz9NIwcLzaiQyZKkcJDrvIkvzhWu7dJHxWwe1iIAAU 2rmBremNjgjsgCAjzpj/O5BpHPSvKAO/m9HGc1pyX2OvwF1/fABH+aW//SWoiqv1IBnq idzTuBBL890mVEMpzAxbaSOBP82+JlEAU1Rs/Kh39FNNYnFhnDqAJNaskhaxrBdErSkH ra8Q== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=KiUaAkV1; spf=pass (google.com: domain of steveawodey@gmail.com designates 2607:f8b0:4864:20::72f as permitted sender) smtp.mailfrom=steveawodey@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-qk1-x72f.google.com (mail-qk1-x72f.google.com. [2607:f8b0:4864:20::72f]) by gmr-mx.google.com with ESMTPS id u189si6344789vkb.2.2019.08.08.13.18.12 for (version=TLS1_3 cipher=AEAD-AES128-GCM-SHA256 bits=128/128); Thu, 08 Aug 2019 13:18:12 -0700 (PDT) Received-SPF: pass (google.com: domain of steveawodey@gmail.com designates 2607:f8b0:4864:20::72f as permitted sender) client-ip=2607:f8b0:4864:20::72f; Received: by mail-qk1-x72f.google.com with SMTP id r4so69800893qkm.13 for ; Thu, 08 Aug 2019 13:18:12 -0700 (PDT) X-Received: by 2002:a37:e40a:: with SMTP id y10mr14906115qkf.134.1565295492571; Thu, 08 Aug 2019 13:18:12 -0700 (PDT) Received: from [172.25.4.75] (EDUROAM-PAT.NET.CMU.EDU. [128.2.149.7]) by smtp.gmail.com with ESMTPSA id 6sm45355475qkp.82.2019.08.08.13.18.10 (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 08 Aug 2019 13:18:11 -0700 (PDT) From: Steve Awodey Message-Id: <728FA1EA-014C-4242-8B34-33A17D7B9208@gmail.com> Content-Type: multipart/alternative; boundary="Apple-Mail=_6CAA8E0B-013C-474F-8BD9-EE42884DA30C" Mime-Version: 1.0 (Mac OS X Mail 11.5 \(3445.9.1\)) Subject: Re: [HoTT] (Beginner's question) Uses of HITs beyond homotopy theory Date: Thu, 8 Aug 2019 16:18:10 -0400 In-Reply-To: Cc: Homotopy Type Theory To: Timothy Carstens References: X-Mailer: Apple Mail (2.3445.9.1) X-Original-Sender: steveawodey@gmail.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=KiUaAkV1; spf=pass (google.com: domain of steveawodey@gmail.com designates 2607:f8b0:4864:20::72f as permitted sender) smtp.mailfrom=steveawodey@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: , --Apple-Mail=_6CAA8E0B-013C-474F-8BD9-EE42884DA30C Content-Transfer-Encoding: quoted-printable Content-Type: text/plain; charset="UTF-8" quotients by equivalence relations. see HoTT Book 6.10 > On Aug 8, 2019, at 2:32 PM, Timothy Carstens wrot= e: >=20 > 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). >=20 > I've got a naive question that I hope isn't too inappropriate for this li= st: can anyone suggest some papers that show applications of HITs? I'm emba= rrassed to admit it, but I don't know any applications outside of synthetic= homotopy theory and higher categories. >=20 > 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!) >=20 > All my best and apologies in advance if this is off-topic for this list, > -t >=20 >=20 > --=20 > 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/msgi= d/HomotopyTypeTheory/CAJGt_zG%2B04Rfbs_py%3DPYkubbwzeYb0TRhhfek-RT663uVUo%3= D-A%40mail.gmail.com . --=20 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 e= mail to HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/= HomotopyTypeTheory/728FA1EA-014C-4242-8B34-33A17D7B9208%40gmail.com. --Apple-Mail=_6CAA8E0B-013C-474F-8BD9-EE42884DA30C Content-Transfer-Encoding: quoted-printable Content-Type: text/html; charset="UTF-8" quotients by equivalenc= e relations.
see HoTT Book 6.10

On Aug 8, 2019, = at 2:32 PM, Timothy Carstens <intoverflow@gmail.com> wrote:

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 f= or 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 st= ill I'm not personally aware of any applied results from that domain (contr= ast with operational semantics; but I am extremely ignorant, so please corr= ect me!)

All my best and apologies in advance if this is off-topic for this l= ist,
-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 e= mail to HomotopyTypeTheory+unsubscribe@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAJGt_zG%2B0= 4Rfbs_py%3DPYkubbwzeYb0TRhhfek-RT663uVUo%3D-A%40mail.gmail.com.

--
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/msg= id/HomotopyTypeTheory/728FA1EA-014C-4242-8B34-33A17D7B9208%40gmail.com.=
--Apple-Mail=_6CAA8E0B-013C-474F-8BD9-EE42884DA30C--