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.1 required=5.0 tests=DKIM_SIGNED,DKIM_VALID, DKIM_VALID_AU,DKIM_VALID_EF,FREEMAIL_FORGED_FROMDOMAIN,FREEMAIL_FROM, HEADER_FROM_DIFFERENT_DOMAINS,HK_RANDOM_FROM,HTML_MESSAGE, MAILING_LIST_MULTI,RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.2 Received: from mail-ot1-x33a.google.com (mail-ot1-x33a.google.com [IPv6:2607:f8b0:4864:20::33a]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 0f83b8aa for ; Thu, 8 Aug 2019 18:52:50 +0000 (UTC) Received: by mail-ot1-x33a.google.com with SMTP id b25sf63496729otp.12 for ; Thu, 08 Aug 2019 11:52:50 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:date:from:to:message-id:in-reply-to:references:subject :mime-version:x-original-sender:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=pTKum1qIMWlbEIgEfgmNBKVbCZT+KvpvpYOB+NgiELE=; b=WQe2ooMumYlyc2hvRga7URuMdwd/Dr6QJYYv+ITyWxPALQ4OcjlMFeoSo66b7SjEzK TX+Eg2sjWvY33Ftjtjdf5FFF5cHYDiZH9zRN4ORFEpBvX8vBN5zmhRkJY46Ho8e6IqmN 1OEYzmnezEvKUXL4+r5EIfyIb5fGeRcKkeh7Chv/APQp+GB42ZuK/wMbu8Ktzz9BeT2i frIL2T1yIWKtUz7ldqulJUfivhZgwbZy2x98Feou8nvO1S4/nxPFZT8Kr66su+kH4ZnR cKeOG3af6K7MzZbsszQ4l5dDoQbjIjrHworBF8c9xopXXoH0aG7ekslk/4QmojINRMbo Xxgg== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=date:from:to:message-id:in-reply-to:references:subject:mime-version :x-original-sender:precedence:mailing-list:list-id:list-post :list-help:list-archive:list-unsubscribe; bh=pTKum1qIMWlbEIgEfgmNBKVbCZT+KvpvpYOB+NgiELE=; b=T1lk+dsBft7gibqdX/bAAhwiF2pvQZNWECvH3VMmYySYvWQLORwf5TasxkWsU7ruHU zWo6+bgkKefa5YVPNrFPTAlA/DUHS1wqR+QvQ/0pDzSe8RJXy6mGAr3JmVFKWp7jyJHt qlQAaxWAulU3KHTyxBLhneICRBfWmiePNO8J+qQaEOcQ9X8YHlORrkFOJh6ujU0mMgmN Zhs8pEEm0WX/aZgteCYWiJ8CHzUPOB29OOsVMAGZg3q4AcExJJDXvSkr2QvKShOinAwP ytIww/s/mQ66h7cnlVegqXOs5xEM+kZ6H4dHAbIJTWfL6eYQkxKRYmVfnPbXkUgZlzaZ SgSQ== 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:in-reply-to :references: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=pTKum1qIMWlbEIgEfgmNBKVbCZT+KvpvpYOB+NgiELE=; b=RbbkFTbmJA59e2on9HTxV+ygQNjs0OINxCQHni5N8weO6odB/4D+fBdiQVbSzJQrlI zMo3+YbZL3iOrR84MuvukEZ5YxEqE+YEnXgBkpERLyYPX4XffcLCYJhtuVusgAIWWm0T E5eveV7YGUwkVWf37XAEf86u+rXUi77fqjtWlH4HAc9UqjfMCGfVpERzciutmIRX0PEx Z9lJRzZqOTQKlwH9bYVyOjQs3K8Fd5zrEbZdCTOfzSzTHRHhfbsxr8dg2urbHRxtjSTj GxBJ6DIU2gFh8FXziXDoI4vmXfG5WG9K3rKzUBhPY9KB3F2iwxxXnqhhWkMeE+9QWL9e v+JQ== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAVIAtkuy8sNK7Dt3TI5B4e++Tdtq3XEaQeqMJZAkM6k5JYWjU9p RGCyxZbJtyGowAq03QKCqnw= X-Google-Smtp-Source: APXvYqy6kfcLo53RJl9Ddo7V/hifatwZgmU5PFx3u8w2Np5Bh+AU7gAbiOj/7pORGHJWZHvWNBI3Xw== X-Received: by 2002:a9d:7352:: with SMTP id l18mr14852299otk.292.1565290369568; Thu, 08 Aug 2019 11:52:49 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a05:6808:6d0:: with SMTP id m16ls11896oih.16.gmail; Thu, 08 Aug 2019 11:52:49 -0700 (PDT) X-Received: by 2002:aca:4309:: with SMTP id q9mr3868052oia.74.1565290369138; Thu, 08 Aug 2019 11:52:49 -0700 (PDT) Date: Thu, 8 Aug 2019 11:52:48 -0700 (PDT) From: Niels van der Weide To: Homotopy Type Theory Message-Id: In-Reply-To: References: Subject: [HoTT] Re: (Beginner's question) Uses of HITs beyond homotopy theory MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_604_876742308.1565290368425" X-Original-Sender: nnmvdw@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: , ------=_Part_604_876742308.1565290368425 Content-Type: multipart/alternative; boundary="----=_Part_605_813445962.1565290368425" ------=_Part_605_813445962.1565290368425 Content-Type: text/plain; charset="UTF-8" Some established applications of HITs outside of synthetic homotopy theory: - Partiality monad, see "Partiality Revisited" by Altenkirch, Danielsson, and Kraus - Type Theory in Type Theory, see 'Type Theory in Type Theory with Quotient Inductive Inductive Types' and 'Normalization by evaluation for dependent types' by Altenkirch and Kaposi - Free algebraic structures, see HoTT book 6.11 and the paper "Finite Sets in Homotopy Type Theory" by Frumin, Geuvers, Gondelman, Van der Weide - Patch theory, see 'Homotopical Patch Theory' by Angiuli, Morehouse, Licata, and Harper On Thursday, August 8, 2019 at 8:33:06 PM UTC+2, Timothy Carstens 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 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/bc0fb45d-fe21-4380-bfcb-70cc58fbeef2%40googlegroups.com. ------=_Part_605_813445962.1565290368425 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Some established applications of HITs outside of synthetic= homotopy theory:
- Partiality monad, see "Partiality Revisited&qu= ot; by Altenkirch, Danielsson, and Kraus
- Type Theory in Type Th= eory, see 'Type Theory in Type Theory with Quotient Inductive Inductive= Types' and 'Normalization by evaluation for dependent types' b= y Altenkirch and Kaposi
- Free algebraic structures, see HoTT book = 6.11 and the paper "Finite Sets in Homotopy Type Theory" by Frumi= n, Geuvers, Gondelman, Van der Weide
- Patch theory, see 'Hom= otopical Patch Theory' by Angiuli, Morehouse, Licata, and Harper
On Thursday, August 8, 2019 at 8:33:06 PM UTC+2, Timothy Carstens wrote:
Sorry for = the broad & naive question. I'm a geometer by training but have bee= n 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 theor= y and higher categories.

Perhaps categorical seman= tics? But even still I'm not personally aware of any applied results fr= om that domain (contrast with operational semantics; but I am extremely ign= orant, 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 &= 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.co= m/d/msgid/HomotopyTypeTheory/bc0fb45d-fe21-4380-bfcb-70cc58fbeef2%40googleg= roups.com.
------=_Part_605_813445962.1565290368425-- ------=_Part_604_876742308.1565290368425--