From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: homotopytypetheory+bncBCHZRD56UYLBBQ4GW7OQKGQENRWYRNA@googlegroups.com X-Spam-Checker-Version: SpamAssassin 3.4.2 (2018-09-13) on inbox.vuxu.org X-Spam-Level: X-Spam-Status: No, score=-0.7 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-pf1-x43b.google.com (mail-pf1-x43b.google.com [IPv6:2607:f8b0:4864:20::43b]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id eefa803e for ; Fri, 28 Sep 2018 05:59:32 +0000 (UTC) Received: by mail-pf1-x43b.google.com with SMTP id a4-v6sf5630830pfi.16 for ; Thu, 27 Sep 2018 22:59:32 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1538114371; cv=pass; d=google.com; s=arc-20160816; b=PRplpvGOeoAVCLaqqPlqe2580RMzrUIuIRJ4pxD3+g8m4SqpgJ7dirbvEuJVnfxuTw vxdxaMtD0lUaimm7InbfaCeTmYNsBSw9ZofZujBsKTzdW8+UTxT4Bn21LlBUavffGGuV xB5aGTTp4cVRedwC9vLp+mnJrcTiLs1yxgWkRF3No4OsEfWI1vungDLfPmx0QW5HwsxG BCAcID2OhkMfC4VwcgtplW7TxjnbT9bo7oK8IQJ34wvLs+DlZB4yHY5DcDqXvWlClMOO cKk+R3VNBAHv1ALmhxO7faqz9jv0eKF8g6QS88QY608dnZMejMMENbNe6x9uQCF06JWP 6FRQ== 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:cc:to:subject:message-id:date:from :in-reply-to:references:mime-version:sender:dkim-signature :dkim-signature; bh=W5xdSzcC/BKM1dJKg9FG1dxSmj4SctNwfrOigLPOm+4=; b=dkkwyMwcIBixkN/6eAk3zDQq92yqd08TtOKlLTv6nS5/q11rSrZmC/ioaeSRotF+e7 +GW4LBL0md3rGbuKhdHQmmsDSs6xe101D1CRvNS2f8Xzc7Pmb4G6YjRRGF26UEEiNLto 2cYCYijaUELHkRCv6FNieXlbAPLhZJ4oBfkcimw9zXFZ+bejAVNGMr7UGSEXB7HToxBl Lm4dj341LrubM3bPZK2W4ZN4O357Z/qhTppYCiUXyalTeDUWY+3VO6t69zdkw+FGFSIm ggzFLatAKyc3R4DUtSXdkpl7mZcNJ18PUWZtDO62GStWpUc7wxS5WTmV+xVuGyHheSZg ljxw== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=TgoCXZwX; spf=pass (google.com: domain of josephcmac@gmail.com designates 2607:f8b0:4864:20::130 as permitted sender) smtp.mailfrom=josephcmac@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:references:in-reply-to:from:date:message-id :subject:to:cc:x-original-sender:x-original-authentication-results :precedence:mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=W5xdSzcC/BKM1dJKg9FG1dxSmj4SctNwfrOigLPOm+4=; b=mesZq0dSl7tCFz8ErgV6a1kIz02692xfUMldNUiydMPs64kKRZq8gMcFvTTGKPYKLJ /3qBdmPoluUguY7kqEUVsYog1By9Y3g+QKIlWyEHVGEnKBHfsv6WXZ5KCldFuMMJXkl2 lkbZmUvjEQ7uzjYXTBAHY5emZlWeiIy6izWybzo/fdtKYWc6/nHqrNEg7hzmFBBPaGoi Xj5xElvAeXxHay4JXzWdvUClidfbN+pxt4Q60f7UorSdVlt4LQbL3zbZF2c8TWxft5xa iQup69LZQKJoTMJkt8lkJg5U64M76nylP4PNy87PKJ6mT67O6ZTH1nezl11zP0Eb83ko sTcQ== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version:references:in-reply-to:from:date:message-id:subject:to :cc:x-original-sender:x-original-authentication-results:precedence :mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=W5xdSzcC/BKM1dJKg9FG1dxSmj4SctNwfrOigLPOm+4=; b=NgR/WlWILRU+JpSAqHBX6d97imtbqqzTbP18x3p4warXE8h6wmOI16/UlmTn3TEsnT HbxYjNvsdphgEsFwuLPf+TIETXU9HFfJEjihi8/f456XvwZL1RKFsRgjqbDWybWDsdi6 oNQ5Lj0CcvoaWhUD8cnfjMT0vJDU3PBtEDAlLkUTMj52JxTSA7Y0jSOWM01CLP+/8EEk XWT5pKW9inUmlHn/NfSxkiljquKXfNS3V1FnGl8JqJw/XY1exAaexOxKEx1jdgzeL8WL CTc88kUEzkOy6IJJJ5UYtxU7ARxEfIg0TuvLf10eFFMzqcEk6PZC2doC5ONTqM8FfDMU xSjw== 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:references:in-reply-to:from :date:message-id:subject:to:cc: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=W5xdSzcC/BKM1dJKg9FG1dxSmj4SctNwfrOigLPOm+4=; b=mJcgVx6GDwOizfhcX4eMoLExAtm7PP33pC0tOaBO1RBKLsTi2v032zikWsMwD1t/nS p4FnHqPI3pDaja4sJVBtZNpE2VDkQb7JZNbJ0NYAKBfSyOnA2zhT6ITpIlDwpVm/9DAs lxcVIjkoo3jRPbwqgROkcaPLFCYr2OyH+lyT5D+pvBRrgx8RoVgsl19q6/o5vwJDcsWX 8SGDAwUNVL7KYKKxzXNw1xbzW821uIPz7RbGGrEpBr4/cnHWzaIPkeGk5RTn2AuOvjuz v7b/XDQvrSnab/RvVl1mPmKUMSSrpynwNeOnC5iJJM+Z+RNvqnPxkZrqDBbEAppUYj7f dHFg== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: ABuFfog/7DGQlhg+optzdMmZznsqwzfoAv+iPevRIqxx3SBlpHojHq90 MiU6S62V0clwcHysVU8r9WY= X-Google-Smtp-Source: ACcGV61hMJQAAEfmTdM48Mal67nozNNboFJvfRq9+CC9z3thMf3sbjFNzCPBE2gDAvDwOksAy7jEWQ== X-Received: by 2002:a65:41c1:: with SMTP id b1-v6mr35535pgq.7.1538114371137; Thu, 27 Sep 2018 22:59:31 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a17:902:421:: with SMTP id 30-v6ls3006469ple.8.gmail; Thu, 27 Sep 2018 22:59:30 -0700 (PDT) X-Received: by 2002:a17:902:690b:: with SMTP id j11-v6mr3850433plk.13.1538114370864; Thu, 27 Sep 2018 22:59:30 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1538114370; cv=none; d=google.com; s=arc-20160816; b=r1kb088+sunND1KI1h/Rxf6RaYVzD3BsExb671jUG333QmmTHnJWwREMCeOXmZNzUK U+3hfZX7wOa0OWo+WYEud2fwMmFWQYNrnd2HHPPsDMXj9C5emdHl7s//AJQY+al1rHRl +nGX6W4dK2Q/hHslz7gyILkdooPF2K3Xqux0y+sD+w65qK9OW9KS9HTvC2kkMw7UdH7V wOciE5LIT0IBWgnbPrco2Vb3V5ry+fMsSW5SAXW9Ela7f1UwkdOTEVLvjo6nPxxdYGFv cPafY+3R47JWDbRJxkuGP9/ZeVamd+AvyBNDYiTE8b6Ib5oh5ataReu+V9K821PQgbAE +/+Q== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=cc:to:subject:message-id:date:from:in-reply-to:references :mime-version:dkim-signature; bh=PeVCvgf17wgDdHaO/VpdzZnEB/PQMnM3nl45N8UJnNE=; b=jCg1fwaRELoGSsLlb6MAZkbbuL6LNznwvpgD22QnTt6wnqoWMJM9jdre/CPk+mHXJl qNjdZ2S/K2j4+KphY9l91VgEBR21zDU27UC5gNFD4irS4JEXhQpHbFfto6iVGP3OXiWn unGAh+6EMZ+FIMNBpJgNFOIV4gVREQyFjbCqxdzlKkr+god6dET9QNVw6s3E2d0rKrmN rr49L84uHzfrr4sfGHSjFm0kevfD5qRl0a0UQ5zLrX8ktHyYPaj8YX4DOhvMiPLzP/Ym mNgrlsPgfw4sHd9GaOI+WUbloH0xKEBi4rGrMbi/zGewV95MvcqnLpu1GRvIorzsZ/uA TmBw== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=TgoCXZwX; spf=pass (google.com: domain of josephcmac@gmail.com designates 2607:f8b0:4864:20::130 as permitted sender) smtp.mailfrom=josephcmac@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-it1-x130.google.com (mail-it1-x130.google.com. [2607:f8b0:4864:20::130]) by gmr-mx.google.com with ESMTPS id f19-v6si149566pff.5.2018.09.27.22.59.30 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 27 Sep 2018 22:59:30 -0700 (PDT) Received-SPF: pass (google.com: domain of josephcmac@gmail.com designates 2607:f8b0:4864:20::130 as permitted sender) client-ip=2607:f8b0:4864:20::130; Received: by mail-it1-x130.google.com with SMTP id 139-v6so1342242itf.0 for ; Thu, 27 Sep 2018 22:59:30 -0700 (PDT) X-Received: by 2002:a24:9f07:: with SMTP id c7-v6mr556423ite.53.1538114370065; Thu, 27 Sep 2018 22:59:30 -0700 (PDT) MIME-Version: 1.0 References: <91b60f0a-e5e3-4216-a422-9b52bb8a4cc7@googlegroups.com> In-Reply-To: <91b60f0a-e5e3-4216-a422-9b52bb8a4cc7@googlegroups.com> From: =?UTF-8?Q?Jos=C3=A9_Manuel_Rodriguez_Caballero?= Date: Fri, 28 Sep 2018 01:59:19 -0400 Message-ID: Subject: [HoTT] the weak infinite groupoid in Simple Type Theory To: HomotopyTypeTheory@googlegroups.com Cc: Joshua Chen Content-Type: multipart/alternative; boundary="000000000000a6da620576e828a9" X-Original-Sender: josephcmac@gmail.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=TgoCXZwX; spf=pass (google.com: domain of josephcmac@gmail.com designates 2607:f8b0:4864:20::130 as permitted sender) smtp.mailfrom=josephcmac@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: , --000000000000a6da620576e828a9 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Recently a user of Isabelle provided his version of HoTT here: https://github.com/jaycech3n/Isabelle-HoTT A brief description from the author: Joshua: > This logic implements intensional Martin-L=C3=B6f type theory with unival= ent > cumulative Russell-style universes, and is > polymorphic. This version of HoTT involves some axiomatization in addition to univalence, e.g., Sum.thy and Prod.thy. HoTT is traditionally developed in CiC, whereas UniMath is traditionally developed in the Martin-L=C3=B6f type theory (as part of CiC in Coq). As a = user of Isabelle/HOL, interested in homotopy type theory, I would like to know the topological interpretation, as a weak infinite groupoid, of Simple Type Theory (the type theory behind Isabelle/HOL) and how it becomes isomorphic to HoTT by means of the axiomatization (maybe there is some topological intuition related to this transformation, cutting and pasting). Thank you in advance, Jos=C3=A9 M. --=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. For more options, visit https://groups.google.com/d/optout. --000000000000a6da620576e828a9 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
=C2=A0 Recently a u= ser of Isabelle provided his version of HoTT here:=C2=A0https://github.com/jaycech3n/Isabelle-H= oTT

=C2=A0 A brief description from the au= thor:=C2=A0

Joshua:
This logic implements intensional Martin-L=C3=B6f type th= eory with univalent cumulative Russell-style universes, and is=C2=A0
pol= ymorphic.

This version of= HoTT involves some axiomatization in addition to univalence, e.g., Sum.thy= and Prod.thy.

=C2=A0 HoTT= is traditionally developed in CiC, whereas UniMath is traditionally develo= ped in the Martin-L=C3=B6f type theory (as part of CiC in Coq). As a user o= f Isabelle/HOL, interested in homotopy type theory, I would like to know th= e topological interpretation, as a weak infinite groupoid, of Simple Type T= heory (the type theory behind Isabelle/HOL) and how it becomes isomorphic t= o HoTT by means of the axiomatization (maybe there is some topological intu= ition related to this transformation, cutting and pasting).

Thank you in advance,
Jos=C3=A9 M.


--
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.
--000000000000a6da620576e828a9--