From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: homotopytypetheory+bncBDTLDGMZRMJBBU7P67NQKGQESP4T74Y@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=-1.1 required=5.0 tests=DKIM_SIGNED,DKIM_VALID, DKIM_VALID_AU,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.1 Received: from mail-oi0-x23a.google.com (mail-oi0-x23a.google.com [IPv6:2607:f8b0:4003:c06::23a]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 3e0dde15 for ; Wed, 22 Aug 2018 23:55:02 +0000 (UTC) Received: by mail-oi0-x23a.google.com with SMTP id w12-v6sf3356343oie.12 for ; Wed, 22 Aug 2018 16:55:02 -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=6F4XK907W3MuwSQbrNjZn4hg+K3kt5VRm8x3A6n44D8=; b=XiTW4ubiXRgPK+lGz159Fz6FrJu564D0P4KobRTmPFp9+gb1wCsOjiyqOragSM4+F/ 5+SYeK0rBSxZA7efag5QKdbhfje5Xvwt4OEjKXskrhpBlNj0hiDQbdoRFM+UR+S1Tuna 0ZvM6/kqdU58TBvZjY65q8c2JqsQpM5UV45Ll/mo5jye+3ReRqQymsYDROWZg9u5t7Zk kdWknqV1ALYWrf+zjHQqTMaJHk6J/T/g7TLo6Xy5D6MhcfDEvcU5/WSFFqPf9Jz9Wuti 4DDIXR6A0U0gbNN1dAfrMjlJmLaieUORFVjNfjF5WN+iX7/egCci/8GbUobaluEVrHGK 6DAQ== 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=6F4XK907W3MuwSQbrNjZn4hg+K3kt5VRm8x3A6n44D8=; b=AOeENV9bzNMujowWh6s8dKrnGzfffuo0mVwhxD2S+YSkKTZlPVpUb/j8SdmzqE04Hq oYobgTARpSLaCCEu7sBSrV0B9IV67ta5Kg6N3n3s/dgy4+jagKepCxSBLv0AFp/Uuccx QuoDv2d2ipvBOmcosH3mnkRkQhwGDaHvOPUweclhSFLh9rsP9dakL89Z2HAA0zkQ6qMQ YDKmifMLn2gi4IUl3ZotlGWZDD09uFdjZgQkSgBCm9ZVjroAikom79TyL9l3X4a5nGol iPOwWGvUOdvE6cLFJ/2lMQA4uD+APsl2xJULmpd0zcHWPJKeHEJ/ehK41alK4OkDTsR+ CJQw== 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=6F4XK907W3MuwSQbrNjZn4hg+K3kt5VRm8x3A6n44D8=; b=MhDhIyLwBVXWU+4o2eV9ItaNdzjpeQppvERI626r5fkNW10owP0xHN0dODraMBye3o vgRZXiA1m5I8ECZ1uvc1mEKWosBxg1C/FAdSCSczyH52E59WrBJqV8R0PKorK8ISRA2j vM5gta0E2IfsUE8yDOHSQyUjqQru15Q3I2SlOnCnYkXkRfV8poPWZW0zg5aXNznKJs95 m3rt1CGR44RijwiPTTq58/NGN81MqnjFHxcFRgnVe5o3IGfST0jw92YSQG0T5IFTj5ux 0J9YAkC9ZdUu//Xyk/uXQsdqdkwa7DFSjMZsW4dbtQOJiY1xGx3N4Qrg2+r1UnH7dJVE NRFQ== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AOUpUlFCS8IruDoq0fupv8yts+nnZHyU7OKGi/gIaH+jI2W+9nLIentC MpNh6nyuKsTtk2iW46hOYs0= X-Google-Smtp-Source: AA+uWPzw+1s8CKS0BMscSl1zrwAol/jvsw2fcJTBPC9rpbq53fIlhwOg6l8pgtwEHeRx9RmmsAYWyQ== X-Received: by 2002:aca:de07:: with SMTP id v7-v6mr1210851oig.5.1534982099841; Wed, 22 Aug 2018 16:54:59 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:aca:1702:: with SMTP id j2-v6ls1622147oii.8.gmail; Wed, 22 Aug 2018 16:54:59 -0700 (PDT) X-Received: by 2002:aca:d417:: with SMTP id l23-v6mr10613oig.7.1534982099392; Wed, 22 Aug 2018 16:54:59 -0700 (PDT) Date: Wed, 22 Aug 2018 16:54:58 -0700 (PDT) From: Corlin Fardal To: Homotopy Type Theory Message-Id: <6f8e170d-0c46-4b2f-a606-2a5ffb5ae3a4@googlegroups.com> In-Reply-To: <45604a7e-3ecd-4caa-90a9-ad8c5a257756@googlegroups.com> References: <45604a7e-3ecd-4caa-90a9-ad8c5a257756@googlegroups.com> Subject: [HoTT] Re: 1D Mu Type MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_2525_980624026.1534982098845" X-Original-Sender: fardalcorlin@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_2525_980624026.1534982098845 Content-Type: multipart/alternative; boundary="----=_Part_2526_795594526.1534982098846" ------=_Part_2526_795594526.1534982098846 Content-Type: text/plain; charset="UTF-8" I could tell that the path algebra was doing something similar to my original coerce function, I was just curious how exactly it worked, with perhaps a breakdown of what each part is doing, and how you even came up with the term in the first place, it seems non-obvious to me, to say the very least. Also, I knew that the choice of putting it on the left or the right was equivalent, I tried to say as much, but seeing as it aligns with what you do in the HIITs paper, I was curious if there was a particular reason you seem to prefer the left over the right. -- 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_2526_795594526.1534982098846 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
I could tell that the path algebra was doing something sim= ilar to my original coerce function, I was just curious how exactly it work= ed, with perhaps a breakdown of what each part is doing, and how you even c= ame up with the term in the first place, it seems non-obvious to me, to say= the very least. Also, I knew that the choice of putting it on the left or = the right was equivalent, I tried to say as much, but seeing as it aligns w= ith what you do in the HIITs paper, I was curious if there was a particular= reason you seem to prefer the left over the right.

--
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_2526_795594526.1534982098846-- ------=_Part_2525_980624026.1534982098845--