From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: homotopytypetheory+bncBCHZRD56UYLBB6GUZLOQKGQEJZWT6ZQ@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-oi1-x23f.google.com (mail-oi1-x23f.google.com [IPv6:2607:f8b0:4864:20::23f]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 5a5a0c02 for ; Mon, 1 Oct 2018 23:15:06 +0000 (UTC) Received: by mail-oi1-x23f.google.com with SMTP id d23-v6sf62609oib.6 for ; Mon, 01 Oct 2018 16:15:05 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1538435705; cv=pass; d=google.com; s=arc-20160816; b=YpzkKQQb2n9sqqr5iAQ8CczmRXVQspj/8mu1bv/+zWeX/U5I7K31zNiShkdPk6+6Bk Zk0co2I/XLv/di67A9HY5HtUa9JV+LekXMzMsSR/NdEISYJWrcd5ckw3EsxBiYUY1bkW iHnBwufW055DxvKV5wjSNyNgFIOPonKp4PXZwypy+3jcD9EFl09eWB6SpvhtEQlUa2v4 wnDOeuJ/TssJt8jOhMqlxkqtWWYjdOSU+EXpyOfkxAhlypO38kty+7QVr7cI+6GmlHio MZxfS2qjFIzKdyU4VZRzPPaAuvdQact5IUpuL5h29b+KvLcO/Tt0rGMGcnQM4WZzRFKN wtVg== 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=YBQn09RU5f4ES0EfrgxXfhbgsDPGqveHIePx3AxRo9M=; b=L4gxcaRbZpojgvNpo//VcJT4kEfcR3GG1xkbaWWQW66vet8pqbq02N76y73LeVgUmm CZ9QlMDNgogSl8d0VUOkA4v6pJtD7HDnh9JLQKkEJhXTDefeJf89VTlDLxp+FNbmeyGb S+g3DjNCcPpZ/oploUwsfv20eF5VClzLqDbbwBaI36TZ5J3VMLXyiyClw5NlFgtbuSao 4+A5WXmCCOhoqZEdBBd1JivR1vujHsalqsnKaC0PvMeiQy4nbt/KXQ3iBifbQ+QUGrfN YXQJMX0HSopzhfC1HLppeVYjg2AW5o7jMlRcIGJrh3BpTy4JsDOGaYzSVAjWGfrbRenr Iuig== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=XrSAoHBf; spf=pass (google.com: domain of josephcmac@gmail.com designates 2607:f8b0:4864:20::12d 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=YBQn09RU5f4ES0EfrgxXfhbgsDPGqveHIePx3AxRo9M=; b=bgkW1lUFIyilHjSHHynlEI/19csbSurDv+i7Y5AZ5C+TxleW49bE4lF995cq+Osbyi k9SJNNP2bthmncFBOFs19iSMR/QV68TYAT916MwYwdlCCDOWh2AGR38vpYp/WFJFx2TG VmZDA5PgOomjWEJSOZePQC3XTjpEub8Dkrcnj03qQKIG2cyr64SarPDFkcYHxDAQb6iC 24rZA5S32IxFMaU+8rM1TjKllCIJvw1ieuz2oiHmoJ6ADjgYMQB+/io7Z/EFNBH6d7+j Rxruc8ew8i+a8K6mu+61vInzEQ5TT0udo8Z44WqlqxNByoudJdj4/4j+8uq2JizbP+Ti m8Lw== 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=YBQn09RU5f4ES0EfrgxXfhbgsDPGqveHIePx3AxRo9M=; b=T/rzsaKKv1zMrIoEgdeSKi6LrRaOW7oll8ObxLr8/a7ZRTgpwrzo7OhYmAmXGkqOiG 2Ii+CJaz0MzHNSlgrghfaGpsMYriDOYP9DF1HDpJt3g9jIJ9tmdd4pZE01Yeq5sxy6uS XjncTdt1/XvHZFVgr9w/aj9ovtDm0mLLmXGMmUDATLE2q+Ht0D57sFGWDTMAQ29sdMrM 0fg8BM8ogPap1rBpV+0OCvLQUrnoF0DKnxKQnBZZOxUYlnHjHO1f11mZ6nOpiLDH8/+d 1Si3pNUJBsmx9XcTbfNpASKB/n8TYqpZ5vvSAmwm2ZtFhqVFmU4J4Ca3q2TTrvGN+Uq2 Cy1w== 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=YBQn09RU5f4ES0EfrgxXfhbgsDPGqveHIePx3AxRo9M=; b=Zg/t4iwT0e9YShpnw7nX2M4zt316NNGCEdCSEjjkhjplXUK/sXidBvEMj2f3XBfxlf tFSt+lNV9k+fairmbGnApajXG9JKVWKH7Ii7K6SwBb9GQYHzpZdkDlVv7jsIz+jQ511m +NVw1oT0zjlIzNQL8/51kHvbnX8VbaHO4Sq36cZY0SE9715JESSH3g1w/wWpG4/rhmIs LdReFD7FC845pLL6b+uenUFuRC8Wk4+JuCHWb8A/YDM7jXJChDtsDz4s2GqcnOhe/nVl kTblQOKSHItstXHwvQ4H5OiBnhsT6VCd9t8dwiQPyOyGqsYQBukDewhrtg9fRdX9kBD6 qOwQ== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: ABuFfoib/PZ10vXEGx3D9VuwWTNGz8gsWFYiepP1HWiy/Op7J0ANUESj rrrk3K7bBIT43yK51BmXFnA= X-Google-Smtp-Source: ACcGV60O/ozDpwEkgfcbJlQSeQ0ZetlOJHw3nZHEuq8Tud1Ph/4MIJI8ASuYDNUscYHI5zZbs0pq5w== X-Received: by 2002:aca:7552:: with SMTP id q79-v6mr205450oic.1.1538435704929; Mon, 01 Oct 2018 16:15:04 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a9d:5512:: with SMTP id l18-v6ls4962739oth.16.gmail; Mon, 01 Oct 2018 16:15:04 -0700 (PDT) X-Received: by 2002:a9d:27c9:: with SMTP id c67-v6mr9981977otb.61.1538435704580; Mon, 01 Oct 2018 16:15:04 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1538435704; cv=none; d=google.com; s=arc-20160816; b=Iq7/gpv4Kc8nbUPqiBtT6UtBjTyAmyLmtq0pzEHY6um91sYT2Lp5Wd6VnZKK1gKk8J V6kNg6ajEAw6H54phQqLydZ4nJ2VqjjdTgI+i62QniAymK5ZzU2AHlI3o4aE3U+gHyvv 81hIa16dSd4vWHwb7EtW+yrpW9Ut4KYCBdF9iHUKLhwDiFABR+An5cdfBvQq4oOOM5gW 976ttU46GVXgBZdHZQNUxZhgfXDzNJ93rY3V/obz8tabt82TXM+MlfOHJbBuJdC69uUc 68LExBT22qxVwqR2Kxo+x2apgkqw9WfvEZ4Yv1FEnk5exukDREeZSFJ/S4nu8a4o/Y+j hlEA== 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=GOcYjDeQOLotz9CMlraflS0tt6hAS/7Z+FgE6Ml+v8U=; b=DiTtUfvDS5esDJWRwu1VoXKxH47a8IFg6aiIQrRLGRnglt31tfoksEJOtg77Z8+b/I e5WvSZpcf/6pLAA9X2V9guVV1zv7VyE1rCPOVxHGkSrvsDYgIrufLNourg4uUHDHzhq6 DKT3RrC7OkHYN/crDMmyHop7nPRb3GtMQmjPBVBsR/ZAEITFfYDwZEowQ220M1/B9T8S f0coLN1F6FWn9YcoHajNLqBkqsMdkWFuKmm6tCcJW4kSetQqyzBfPkIx3r2NIJ+rL+Zb BSjR08pRy07/Q5WH45Z0wS2SJEDTsZCVH0MxGbgXH5bCJMlUYeAGqe3U6S5Fwn5SGsDd tXCQ== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=XrSAoHBf; spf=pass (google.com: domain of josephcmac@gmail.com designates 2607:f8b0:4864:20::12d as permitted sender) smtp.mailfrom=josephcmac@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-it1-x12d.google.com (mail-it1-x12d.google.com. [2607:f8b0:4864:20::12d]) by gmr-mx.google.com with ESMTPS id n206-v6si481654oib.4.2018.10.01.16.15.04 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Mon, 01 Oct 2018 16:15:04 -0700 (PDT) Received-SPF: pass (google.com: domain of josephcmac@gmail.com designates 2607:f8b0:4864:20::12d as permitted sender) client-ip=2607:f8b0:4864:20::12d; Received: by mail-it1-x12d.google.com with SMTP id i76-v6so756775ita.3 for ; Mon, 01 Oct 2018 16:15:04 -0700 (PDT) X-Received: by 2002:a02:698b:: with SMTP id e133-v6mr9700072jac.119.1538435703986; Mon, 01 Oct 2018 16:15:03 -0700 (PDT) MIME-Version: 1.0 References: <91b60f0a-e5e3-4216-a422-9b52bb8a4cc7@googlegroups.com> <6535A055-1DC4-42AD-A0EB-37B1D523ECA1@cmu.edu> In-Reply-To: <6535A055-1DC4-42AD-A0EB-37B1D523ECA1@cmu.edu> From: =?UTF-8?Q?Jos=C3=A9_Manuel_Rodriguez_Caballero?= Date: Mon, 1 Oct 2018 19:14:52 -0400 Message-ID: Subject: Re: [HoTT] the weak infinite groupoid in Simple Type Theory To: HomotopyTypeTheory@googlegroups.com Cc: Joshua Chen Content-Type: multipart/alternative; boundary="000000000000a56197057732f900" 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=XrSAoHBf; spf=pass (google.com: domain of josephcmac@gmail.com designates 2607:f8b0:4864:20::12d 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: , --000000000000a56197057732f900 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable > > Mike wrote: > If you > think of the types as spaces up to homotopy, then you get sort of a > truncated version of HoTT, where the predicates are unions of > connected components, and in which probably not very much that's > actually homotopical can be said without dependent types. Indeed, I think that the lemma lemma card_permutations: assumes "card S =3D n" and "finite S" shows "card {p. p permutes S} =3D fact n" in HOL/Library/Permutations.thy is a truncation of the following theorem due to Voevodsky Theorem weqfromweqstntostn ( n : nat ) : ( (=E2=9F=A6n=E2=9F=A7) =E2=89=83 = (=E2=9F=A6n=E2=9F=A7) ) =E2=89=83 =E2=9F=A6factorial n=E2=9F=A7. which can be found here: https://github.com/UniMath/UniMath/blob/master/UniMath/Combinatorics/Standa= rdFiniteSets.v By the way, I do not know if the project of developing combinatorics from homotopy type theory, started by Voevodsky, continues today or if it stopped. Kind Regards, Jos=C3=A9 M. El lun., 1 oct. 2018 a las 10:53, Steve Awodey () escribi= =C3=B3: > of course, there are also topological models of simple type theory resp. > HOL, and extensional MLTT, which are then not homotopical. > See e.g.: > > https://arxiv.org/abs/math/9707206 > > Steve > > On Oct 1, 2018, at 10:43 AM, Michael Shulman wrote= : > > Simple type theory also has topological / homotopical models, but less > of the structure is visible to them. If you think of the types as > topological spaces up to homeomorphism, then you get something > approaching "synthetic topology", where the "predicates" can be > (depending on the rules) either injective continuous functions or > subspace embeddings. (Note that this approach is incompatible with > classical logic, which I believe is built into Isabelle/HOL.) If you > think of the types as spaces up to homotopy, then you get sort of a > truncated version of HoTT, where the predicates are unions of > connected components, and in which probably not very much that's > actually homotopical can be said without dependent types. > On Fri, Sep 28, 2018 at 1:28 PM Jos=C3=A9 Manuel Rodriguez Caballero > wrote: > > > Dear Mike, > Thank you for the elucidation with respect to my confusions concerning > type theory and proof assistants. I use Isabelle/HOL in a practical way i= n > order to formalize my own mathematical results in number theory and > language theory, but I am a beginner with respect to the theory behind > proof assistants. > > I watched some lectures of Voevodsky using topological reasoning in > homotopy type theory, e.g., talking about the homotopy fiber and drawing > some pictures. I like the topological language, because I am mathematicia= n > rather than computer scientist. So, it would be wonderful for me to use > topological language and maybe topological intuition when I am programmin= g > in Isabelle/HOL (simple type theory). But I am not sure if this is possib= le. > > Kind Regards, > Jose M. > > > > El vie., 28 sept. 2018 a las 15:21, Michael Shulman () > escribi=C3=B3: > > > It sounds like there are several misconceptions here. > > Firstly, many different type theories are used in the subject of > homotopy type theory, but CiC is not really one of them. In addition > to inductive types, CiC is distinguished by a primitive impredicative > universe of propositions, whereas (almost?) all work in HoTT instead > defines the "propositions" to be the homotopy (-1)-types. Coq is a > proof assistant that implements CiC, and Coq is also often used to > formalize HoTT -- but only by ignoring the universe Prop (indeed, we > had to get the Coq developers to implement a special flag for HoTT to > *enable* us to ignore Prop). So even though HoTT is often formalized > in Coq, I think it's misleading to say that CiC is so used. UniMath > is a particular library which formalizes a particular approach to HoTT > in Coq, using roughly only the MLTT core plus univalence; other > libraries for Coq in HoTT also use inductive types and axioms for > HITs. > > Secondly, I expect you probably know this even better than I do, but > Isabelle (or Isabelle/Pure) is distinct from Isabelle/HOL: > Isabelle/Pure is a "logical framework" in which one can specify and > work with many different object theories, of which HOL is only one. > It appears that Josh's development is such a theory, so rather than > "HoTT in Isabelle/HOL" it is "HoTT in Isabelle/Pure", or one might say > "Isabelle/HoTT" -- it's not really related at all to Isabelle/HOL > except that they are both formalized in the same logical framework. > > Finally, specifying HoTT inside of a logical framework does not make > the logical framework "isomorphic" to HoTT (I'm not even sure what > that would mean), nor does it directly give a topological or > higher-groupoidal interpretation of the framework. In particular, > Josh's Isabelle encoding of HoTT is (like the earlier encoding > Isabelle/CTT of an extensional dependent type theory, > https://isabelle.in.tum.de/dist/library/CTT/index.html) what some > LF-theorists call "synthetic" > (https://ncatlab.org/nlab/show/logical+framework#Synthetic), which > means that it is an encoding of the *untyped syntax* together with the > typing judgments. So I think it is not very different, from a > semantic perspective, from formulating the syntax of HoTT inside, say, > ZFC; in particular it doesn't imply any relationship between the > semantics of the object-language and the meta-language. (The > advantage of a logical framework like Isabelle/Pure over ZFC for this > purpose is the availability of higher-order abstract syntax to > represent variable binding.) > > If one uses a logical framework "analytically" instead > (https://ncatlab.org/nlab/show/logical+framework#Analytic), then there > can be a closer connection between the semantics of the framework and > the object language. However, I believe that such an encoding of a > *dependent* type theory is only possible in a framework that is also > dependently typed, unlike Isabelle. > > I hope this helps answer your questions; if I misunderstood what you > were asking, please ask again! > > Mike > > On Thu, Sep 27, 2018 at 10:59 PM Jos=C3=A9 Manuel Rodriguez Caballero > wrote: > > > 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 Ty= pe > Theory (the type theory behind Isabelle/HOL) and how it becomes isomorphi= c > 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. > > > -- > 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. > > > -- > 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. > > > -- > 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. > > > --=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. --000000000000a56197057732f900 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Mike wrote:
If you
think o= f the types as spaces up to homotopy, then you get sort of a
truncated v= ersion of HoTT, where the predicates are unions of
connected components,= and in which probably not very much that's
actually homotopical can= be said without dependent types.

Indeed, I= think that the lemma

lemma card_permutations= :
=C2=A0 assumes "card S =3D n"
=C2=A0 =C2=A0= and "finite S"
=C2=A0 shows "card {p. p permutes = S} =3D fact n"

in HOL/Library/Permutations.th= y

is a truncation of the following theorem d= ue to Voevodsky

Theorem weqfromweqstntostn ( n : n= at ) : ( (=E2=9F=A6n=E2=9F=A7) =E2=89=83 (=E2=9F=A6n=E2=9F=A7) ) =E2=89=83 = =E2=9F=A6factorial n=E2=9F=A7.


=
By the way, I do not know if the project of developing combinato= rics from homotopy type theory, started by Voevodsky, continues today or if= it stopped.

Kind Regards,
Jos=C3=A9 M.= =C2=A0


El lun., 1 oct. 2018 a las 10:53, Steve Awodey (<= ;awodey@cmu.edu>) escribi=C3=B3:
of course, there are also topological models o= f simple type theory resp. HOL, and extensional MLTT, which are then not ho= motopical.=C2=A0
See e.g.:


Steve

On Oct 1, 2018, at 10:43 AM, Michael Shulman <shulman@sandiego.edu> wrote:<= /div>
Simple type theory also has topological / homotopical models, but lessof the structure is visible to them.=C2=A0 If you think of the types astopological spaces up to homeomorphism, then you get something
approach= ing "synthetic topology", where the "predicates" can be=
(depending on the rules) either injective continuous functions or
su= bspace embeddings. =C2=A0(Note that this approach is incompatible with
c= lassical logic, which I believe is built into Isabelle/HOL.) =C2=A0If youthink of the types as spaces up to homotopy, then you get sort of a
tr= uncated version of HoTT, where the predicates are unions of
connected co= mponents, and in which probably not very much that's
actually homoto= pical can be said without dependent types.
On Fri, Sep 28, 2018 at 1:28 = PM Jos=C3=A9 Manuel Rodriguez Caballero
<josephcmac@gmail.com> wrote:

Dear Mike,
=C2=A0Thank you for the elucidation = with respect to my confusions concerning type theory and proof assistants. = I use Isabelle/HOL in a practical way in order to formalize my own mathemat= ical results in number theory and language theory, but I am a beginner with= respect to the theory behind proof assistants.

I watched some lectu= res of Voevodsky using topological reasoning in homotopy type theory, e.g.,= talking about the homotopy fiber and drawing some pictures. I like the top= ological language, because I am mathematician rather than computer scientis= t. So, it would be wonderful for me to use topological language and maybe t= opological intuition when I am programming in Isabelle/HOL (simple type the= ory). But I am not sure if this is possible.

Kind Regards,
Jose M= .



El vie., 28 sept. 2018 a las 15:21, Michael Shulman (<<= a href=3D"mailto:shulman@sandiego.edu" target=3D"_blank">shulman@sandiego.e= du>) escribi=C3=B3:

It sounds like = there are several misconceptions here.

Firstly, many different type = theories are used in the subject of
homotopy type theory, but CiC is not= really one of them.=C2=A0 In addition
to inductive types, CiC is distin= guished by a primitive impredicative
universe of propositions, whereas (= almost?) all work in HoTT instead
defines the "propositions" t= o be the homotopy (-1)-types.=C2=A0 Coq is a
proof assistant that implem= ents CiC, and Coq is also often used to
formalize HoTT -- but only by ig= noring the universe Prop (indeed, we
had to get the Coq developers to im= plement a special flag for HoTT to
*enable* us to ignore Prop).=C2=A0 So= even though HoTT is often formalized
in Coq, I think it's misleadin= g to say that CiC is so used.=C2=A0 UniMath
is a particular library whic= h formalizes a particular approach to HoTT
in Coq, using roughly only th= e MLTT core plus univalence; other
libraries for Coq in HoTT also use in= ductive types and axioms for
HITs.

Secondly, I expect you probabl= y know this even better than I do, but
Isabelle (or Isabelle/Pure) is di= stinct from Isabelle/HOL:
Isabelle/Pure is a "logical framework&quo= t; in which one can specify and
work with many different object theories= , of which HOL is only one.
It appears that Josh's development is su= ch a theory, so rather than
"HoTT in Isabelle/HOL" it is "= ;HoTT in Isabelle/Pure", or one might say
"Isabelle/HoTT"= -- it's not really related at all to Isabelle/HOL
except that they = are both formalized in the same logical framework.

Finally, specifyi= ng HoTT inside of a logical framework does not make
the logical framewor= k "isomorphic" to HoTT (I'm not even sure what
that would = mean), nor does it directly give a topological or
higher-groupoidal inte= rpretation of the framework.=C2=A0 In particular,
Josh's Isabelle en= coding of HoTT is (like the earlier encoding
Isabelle/CTT of an extensio= nal dependent type theory,
https://isabelle.in.tum.de/dist/lib= rary/CTT/index.html) what some
LF-theorists call "synthetic&quo= t;
(https://ncatlab.org/nlab/show/logical+framework#Synthet= ic), which
means that it is an encoding of the *untyped syntax* toge= ther with the
typing judgments.=C2=A0 So I think it is not very differen= t, from a
semantic perspective, from formulating the syntax of HoTT insi= de, say,
ZFC; in particular it doesn't imply any relationship betwee= n the
semantics of the object-language and the meta-language. =C2=A0(The=
advantage of a logical framework like Isabelle/Pure over ZFC for thispurpose is the availability of higher-order abstract syntax to
represe= nt variable binding.)

If one uses a logical framework "analytic= ally" instead
(https://ncatlab.org/nlab/show/logical+fr= amework#Analytic), then there
can be a closer connection between the= semantics of the framework and
the object language.=C2=A0 However, I be= lieve that such an encoding of a
*dependent* type theory is only possibl= e in a framework that is also
dependently typed, unlike Isabelle.
I hope this helps answer your questions; if I misunderstood what you
we= re asking, please ask again!

Mike

On Thu, Sep 27, 2018 at 10:= 59 PM Jos=C3=A9 Manuel Rodriguez Caballero
<josephcmac@gmail.com> wrote:

=C2=A0Recently a user of Isabelle provided his = version of HoTT here: https://github.com/jaycech3n/Isabelle-HoTT

= =C2=A0A brief description from the author:

Joshua:
This logic implements intensional Martin-L=C3=B6f type theory w= ith univalent 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.

=C2=A0HoTT is t= raditionally developed in CiC, whereas UniMath is traditionally developed i= n the Martin-L=C3=B6f type theory (as part of CiC in Coq). As a user of Isa= belle/HOL, interested in homotopy type theory, I would like to know the top= ological interpretation, as a weak infinite groupoid, of Simple Type Theory= (the type theory behind Isabelle/HOL) and how it becomes isomorphic to HoT= T 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.


--
You received this message because= you are subscribed to the Google Groups "Homotopy Type Theory" g= roup.
To unsubscribe from this group and stop receiving emails from it, = send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com<= /a>.
For more options, visit https://groups.google.com/d/optout.

--
You received this message because you are subscri= bed to the Google Groups "Homotopy Type Theory" group.
To unsu= bscribe from this group and stop receiving emails from it, send an email to= HomotopyTypeTheory+unsubscribe@googlegroups.com.
For mor= e options, visit https://groups.google.com/d/optout.

--
Y= ou received this message because you are subscribed to the Google Groups &q= uot;Homotopy Type Theory" group.
To unsubscribe from this group and= stop receiving emails from it, send an email to HomotopyTypeTheo= ry+unsubscribe@googlegroups.com.
For more options, visit https://groups.google= .com/d/optout.

=

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