From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: homotopytypetheory+bncBDWYNQEA54IRBVPJZDOQKGQEFJV5GHI@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.9 required=5.0 tests=DKIMWL_WL_MED,DKIM_SIGNED, DKIM_VALID,DKIM_VALID_EF,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-wm1-x33a.google.com (mail-wm1-x33a.google.com [IPv6:2a00:1450:4864:20::33a]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id d7b9220b for ; Mon, 1 Oct 2018 14:53:10 +0000 (UTC) Received: by mail-wm1-x33a.google.com with SMTP id l66-v6sf9360137wmb.1 for ; Mon, 01 Oct 2018 07:53:10 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1538405589; cv=pass; d=google.com; s=arc-20160816; b=CnqdkIIBL6qrtl4xG/LrchYhTukIZR+EGQDs8uBR9EDqT/0Zlbb70vemg8gjsFziSb pbr7CjttVWojndCyM5j8EmmpixpteLBNsaVml90L21AecZFHQSznBlO4fs1yDKdTcDIj 5oxcHTA5Ejj23n1e6oD/nf5V8Sw39ff+AUKf4MzF9HsWk34I0dVO6TKbSvnT5xkDMXuj y0fl4Mq01RURKKioOV6zDPpRMAHPIT+d4MkDd6Pe1JE9EvZEG4zQBUh/vd0actfRSmmI kPcnm/b+pwo3w+io63QA5btwodiAWACjHFZRK1Lc98WvXRxBhr0LlvEa8NSGroy+TM2D mX5g== 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; bh=tXXjZAdvmhAM/lvL4DbJemYr5Ab18p6tGOBr+E80vzw=; b=fPPohM4H662QeHKbz9HbhTDYL9RVhTObFKOgI2vmLcJkzS/gXjWftqZHS/rm7B7MWl 3hVSv1xTSxaH9D8//ENyK8jD2VgVDZOghdtrJTDkdQOGXt1tgQooNGwJfoh6hfpPRnhC eu+4a2yKZeAvIaUBd7NET1CHewxo93ULqDdPYXKxT4qc5znfb2ae8By1oGYdRq9ZulxR 2YQp7/CPjzBFsP2gl/yJTOoGAv0kTJTyLJ6xOQ2KJ+LIUrZnuqrKoQsi4unxzXKRTZjN +sr0iEREK9Bch0RW8F29OqMeUtAQBfUskVCIa3cSwQ1AMEgKrELiY4CLdHokTRBZA/q+ CKOA== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@cmu-edu.20150623.gappssmtp.com header.s=20150623 header.b="D/YBtkuH"; spf=pass (google.com: domain of awodey@andrew.cmu.edu designates 2a00:1450:4864:20::534 as permitted sender) smtp.mailfrom=awodey@andrew.cmu.edu; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=cmu.edu 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=tXXjZAdvmhAM/lvL4DbJemYr5Ab18p6tGOBr+E80vzw=; b=b41gymQm/DtHxD98Jb+/N2N4wkiiuti/1uAAnT/eLla6J9BkQ3lt8U/Fm4P/e4Vbuw 3wyLGzyGy+OR5SkABPGD6P35wSIkZvHh35QolREDTK3TpiBphiXh+ED3LhfKUblybfco 2QHMFxEiZ0eYvEiS9lbDWfcffVSP0/TsLz2l5l2KApWQVtxUcYvjnhVRiBhioxBWmfDn 84VJ2mOk3oupLUawj7qeRKARqAj4rtCtb4RVWJYuKBPhrGMHArnNitYWJlYT4Pw5xlFO 1Pk5W4FJe/2pqf039emJsteeBQ14SYErFXsz02skOcktbFYR3YWmUcHxKrtaPdczBeAU Nj5A== 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=tXXjZAdvmhAM/lvL4DbJemYr5Ab18p6tGOBr+E80vzw=; b=rwZiueVHL29fPgtkoSZgzFDr57Td5J92HoehqytDSdCbVaq5hbsw18mV3W2CVNKKDT 6iFZIxH6hpnxY2GzDTmEeFAj9rE1WjWIb4vplc1Avqn+H5tYRI1999m0QhNz07tAJEjo CTA+HnrGLJCr9hOtZ42vlDRORKgySRcaPJUDv29pebxDPHwmsRlNDpxtn+5mAKoimL1w jzo6ipbQrD3VHcgLwNciPRegZ3rV7f0jbJ0Il/vezEyPy99i8nRWoDWOnPHXneWycbZ1 q9SrAY3Wnt2LeoG8hAuzhYWUe/knFMOWbKXOvD/d4TYznntRSVJi/AtemPIzeILLmfky e6yA== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: ABuFfohXz30A/EWQNYEiue1aXBZK4zxLhl0dmqzP5WtObVZIizSR+bp+ PBbL+ZXbWp8PONvzWbfNCQ0= X-Google-Smtp-Source: ACcGV63Lf1mAPoMmY+35LzVXKtS3tZzBd88HEbKHD2DayamkreS/135M4mgGp9X5/PzlYZzaS+zK+Q== X-Received: by 2002:a5d:51c6:: with SMTP id n6-v6mr135635wrv.0.1538405589905; Mon, 01 Oct 2018 07:53:09 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a1c:23d0:: with SMTP id j199-v6ls48510wmj.18.gmail; Mon, 01 Oct 2018 07:53:09 -0700 (PDT) X-Received: by 2002:a1c:d085:: with SMTP id h127-v6mr1686731wmg.24.1538405589173; Mon, 01 Oct 2018 07:53:09 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1538405589; cv=none; d=google.com; s=arc-20160816; b=Kesxf7X/rpAXUIt+arriZjDUgnMopY+OqlHRDXQ48hQIBIpYDd2BNE9tmkT2zw3MsD mXy7duVn0TfR0bVMxt7xF3Il7sT/Emm0llPVkLim10DqXLwFfpeZ/LytrzWbhg5q6et8 CTXv7rjba8++RYtRqBpC8hvlY0bK37nq6kY4tJb2JciZBEgrbhCWYyEgv4yHpT7WZ4PF tzGZSC/Wfie1V9/uTTwY7CZdWHgnZm1X1e08mVa5vZcM+8RqiwOU9FO9hMZHmUYDtPQI z/Nw+7l12FJ3GMyhgA8lmwxJN4Zj0ZuJ+OOu6ybqu7AT42OCDH07bMVe3s7IdEkpwr8/ wG3w== 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=kJ69CJRBfwr6lOsvHUzM6KOOm4oRTYrs0lHWX8TNRu8=; b=wni0HY9t/lCIMxQnwwePiWjPysarCkJdwv/6AcdLAuJB5MZpNmESwwcaA4/dnTq2ov eUr6ywsiV8phFCJrHE2OJ8bhddgcLAIAtZgewF1h5dBmMKz4UMa5WyZvRjUW4ADLWA7E 94zVcMeoLNHBg934bRSLqEQbyabgyfeIiw1pwZzN35JfEhNOmgsuPNWM7aDPNOrKXxJi 7GNmJpTfilMN00gZGP6Z4MEqF7SVmzrGERfNhZ1sIeID/dG2IYk/c71QeL0w8DunJPfB RWz/l0bN8c4TEwoPW9pH+p0ZQjV2uRRS7b+Mp03j7f0EE/OAfEN6ArWIkS3Z7brLFJ9h N1WQ== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@cmu-edu.20150623.gappssmtp.com header.s=20150623 header.b="D/YBtkuH"; spf=pass (google.com: domain of awodey@andrew.cmu.edu designates 2a00:1450:4864:20::534 as permitted sender) smtp.mailfrom=awodey@andrew.cmu.edu; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=cmu.edu Received: from mail-ed1-x534.google.com (mail-ed1-x534.google.com. [2a00:1450:4864:20::534]) by gmr-mx.google.com with ESMTPS id t1-v6si457436wmi.0.2018.10.01.07.53.09 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Mon, 01 Oct 2018 07:53:09 -0700 (PDT) Received-SPF: pass (google.com: domain of awodey@andrew.cmu.edu designates 2a00:1450:4864:20::534 as permitted sender) client-ip=2a00:1450:4864:20::534; Received: by mail-ed1-x534.google.com with SMTP id q19-v6so14506528edr.1 for ; Mon, 01 Oct 2018 07:53:09 -0700 (PDT) X-Received: by 2002:a05:6402:382:: with SMTP id o2mr3204504edv.42.1538405588784; Mon, 01 Oct 2018 07:53:08 -0700 (PDT) Received: from samson.phil.cmu.edu (SAMSON.PHIL.CMU.EDU. [128.2.65.128]) by smtp.gmail.com with ESMTPSA id s36-v6sm3037800edm.15.2018.10.01.07.53.07 (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Mon, 01 Oct 2018 07:53:08 -0700 (PDT) From: Steve Awodey Message-Id: <6535A055-1DC4-42AD-A0EB-37B1D523ECA1@cmu.edu> Content-Type: multipart/alternative; boundary="Apple-Mail=_293D0AF5-E8AF-46EA-9A05-7BE46C55978B" Mime-Version: 1.0 (Mac OS X Mail 11.3 \(3445.6.18\)) Subject: Re: [HoTT] the weak infinite groupoid in Simple Type Theory Date: Mon, 1 Oct 2018 10:53:05 -0400 In-Reply-To: Cc: josephcmac@gmail.com, "HomotopyTypeTheory@googlegroups.com" , joshua.chen@uni-bonn.de To: Michael Shulman References: <91b60f0a-e5e3-4216-a422-9b52bb8a4cc7@googlegroups.com> X-Mailer: Apple Mail (2.3445.6.18) X-Original-Sender: awodey@cmu.edu X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@cmu-edu.20150623.gappssmtp.com header.s=20150623 header.b="D/YBtkuH"; spf=pass (google.com: domain of awodey@andrew.cmu.edu designates 2a00:1450:4864:20::534 as permitted sender) smtp.mailfrom=awodey@andrew.cmu.edu; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=cmu.edu 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=_293D0AF5-E8AF-46EA-9A05-7BE46C55978B Content-Transfer-Encoding: quoted-printable Content-Type: text/plain; charset="UTF-8" of course, there are also topological models of simple type theory resp. HO= L, and extensional MLTT, which are then not homotopical.=20 See e.g.: https://arxiv.org/abs/math/9707206 Steve > On Oct 1, 2018, at 10:43 AM, Michael Shulman wrote= : >=20 > 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: >>=20 >> 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 in = order to formalize my own mathematical results in number theory and languag= e theory, but I am a beginner with respect to the theory behind proof assis= tants. >>=20 >> I watched some lectures of Voevodsky using topological reasoning in homo= topy type theory, e.g., talking about the homotopy fiber and drawing some p= ictures. I like the topological language, because I am mathematician rather= than computer scientist. So, it would be wonderful for me to use topologic= al language and maybe topological intuition when I am programming in Isabel= le/HOL (simple type theory). But I am not sure if this is possible. >>=20 >> Kind Regards, >> Jose M. >>=20 >>=20 >>=20 >> El vie., 28 sept. 2018 a las 15:21, Michael Shulman () escribi=C3=B3: >>>=20 >>> It sounds like there are several misconceptions here. >>>=20 >>> 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. >>>=20 >>> 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. >>>=20 >>> 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.) >>>=20 >>> 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. >>>=20 >>> I hope this helps answer your questions; if I misunderstood what you >>> were asking, please ask again! >>>=20 >>> Mike >>>=20 >>> On Thu, Sep 27, 2018 at 10:59 PM Jos=C3=A9 Manuel Rodriguez Caballero >>> wrote: >>>>=20 >>>> Recently a user of Isabelle provided his version of HoTT here: https:= //github.com/jaycech3n/Isabelle-HoTT >>>>=20 >>>> A brief description from the author: >>>>=20 >>>>> Joshua: >>>>> This logic implements intensional Martin-L=C3=B6f type theory with un= ivalent cumulative Russell-style universes, and is >>>>> polymorphic. >>>>=20 >>>>=20 >>>> This version of HoTT involves some axiomatization in addition to univa= lence, e.g., Sum.thy and Prod.thy. >>>>=20 >>>> HoTT is traditionally developed in CiC, whereas UniMath is traditiona= lly developed in the Martin-L=C3=B6f type theory (as part of CiC in Coq). A= s a user of Isabelle/HOL, interested in homotopy type theory, I would like = to know the topological interpretation, as a weak infinite groupoid, of Sim= ple Type Theory (the type theory behind Isabelle/HOL) and how it becomes is= omorphic to HoTT by means of the axiomatization (maybe there is some topolo= gical intuition related to this transformation, cutting and pasting). >>>>=20 >>>> Thank you in advance, >>>> Jos=C3=A9 M. >>>>=20 >>>>=20 >>>> -- >>>> You received this message because you are subscribed to the Google Gro= ups "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 Group= s "Homotopy Type Theory" group. >> To unsubscribe from this group and stop receiving emails from it, send a= n email to HomotopyTypeTheory+unsubscribe@googlegroups.com. >> For more options, visit https://groups.google.com/d/optout. >=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. > 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. --Apple-Mail=_293D0AF5-E8AF-46EA-9A05-7BE46C55978B Content-Transfer-Encoding: quoted-printable Content-Type: text/html; charset="UTF-8" of course, there are also = topological models of simple type theory resp. HOL, and extensional MLTT, w= hich are then not homotopical. 
See e.g.:

https://arxiv.org/abs/math/9707206=

Steve

On Oct 1, 2018, at 10:43 AM, Michael Shulman <shulman@sandiego.edu> 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 somet= hing
approaching "synthetic topology", where the "predicates"= can be
(depending on the rules) either injective continuous = functions or
subspace embeddings.  (Note that this appro= ach 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 versi= on of HoTT, where the predicates are unions of
connected comp= onents, and in which probably not very much that's
actually h= omotopical can be said without dependent types.
On Fri, Sep 2= 8, 2018 at 1:28 PM Jos=C3=A9 Manuel Rodriguez Caballero
<<= a href=3D"mailto:josephcmac@gmail.com" class=3D"">josephcmac@gmail.com&= gt; wrote:

Dear Mike,
 Thank you for the elucidation with respec= t to my confusions concerning type theory and proof assistants. I use Isabe= lle/HOL in a practical way in order to formalize my own mathematical result= s 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 th= eory, e.g., talking about the homotopy fiber and drawing some pictures. I l= ike the topological language, because I am mathematician rather than comput= er scientist. So, it would be wonderful for me to use topological language = and maybe topological intuition when I am programming in Isabelle/HOL (simp= le type theory). But I am not sure if this is possible.

Kind Regards,
Jose M.

=

El vie., 28 sept. 2018 a las 15:21, Michael S= hulman (<shulman@sand= iego.edu>) escribi=C3=B3:

It sounds like there are several misconceptions her= e.

Firstly, many different type theories are u= sed in the subject of
homotopy type theory, but CiC is not re= ally one of them.  In addition
to inductive types, CiC i= s distinguished by a primitive impredicative
universe of prop= ositions, 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 toformalize HoTT -- but only by ignoring the universe Prop (indee= d, we
had to get the Coq developers to implement a special fl= ag for HoTT to
*enable* us to ignore Prop).  So even tho= ugh HoTT is often formalized
in Coq, I think it's misleading = to say that CiC is so used.  UniMath
is a particular lib= rary which formalizes a particular approach to HoTT
in Coq, u= sing roughly only the MLTT core plus univalence; other
librar= ies for Coq in HoTT also use inductive types and axioms for
H= ITs.

Secondly, I expect you probably know this= even better than I do, but
Isabelle (or Isabelle/Pure) is di= stinct from Isabelle/HOL:
Isabelle/Pure is a "logical framewo= rk" in which one can specify and
work with many different obj= ect theories, of which HOL is only one.
It appears that Josh'= s development is such a theory, so rather than
"HoTT in Isabe= lle/HOL" it is "HoTT in Isabelle/Pure", or one might say
"Isa= belle/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 framewo= rk 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 th= e framework.  In particular,
Josh's Isabelle encoding of= HoTT is (like the earlier encoding
Isabelle/CTT of an extens= ional dependent type theory,
https://isabelle.in.tum.de/di= st/library/CTT/index.html) what some
LF-theorists call "s= ynthetic"
(https://ncatlab.org/nlab/show/logical+framew= ork#Synthetic), which
means that it is an encoding of the= *untyped syntax* together with the
typing judgments.  S= o I think it is not very different, from a
semantic perspecti= ve, from formulating the syntax of HoTT inside, say,
ZFC; in = particular it doesn't imply any relationship between the
sema= ntics 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 torepresent variable binding.)

If o= ne uses a logical framework "analytically" instead
(ht= tps://ncatlab.org/nlab/show/logical+framework#Analytic), then there
can be a closer connection between the semantics of the framewor= k 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, 20= 18 at 10:59 PM Jos=C3=A9 Manuel Rodriguez Caballero
<josephcmac@gmail.com> = wrote:

&= nbsp;Recently a user of Isabelle provided his version of HoTT here: https://github.c= om/jaycech3n/Isabelle-HoTT

 A brief = description from the author:

Joshua:
This logic implements intensiona= l Martin-L=C3=B6f type theory with univalent cumulative Russell-style unive= rses, 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 tra= ditionally 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 woul= d like to know the topological interpretation, as a weak infinite groupoid,= of Simple Type Theory (the type theory behind Isabelle/HOL) and how it bec= omes 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.


--
You rec= eived this message because you are subscribed to the Google Groups "Homotop= y Type Theory" group.
To unsubscribe from this group and stop= receiving emails from it, send an email to HomotopyTypeTheory+unsubscri= be@googlegroups.com.
For more options, visit https://groups.google.com/d/o= ptout.

--
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 HomotopyTypeT= heory+unsubscribe@googlegroups.com.
For more options, vis= it https://groups= .google.com/d/optout.

--
You received this message because you are subscribed to the Goog= le Groups "Homotopy Type Theory" group.
To unsubscribe from t= his group and stop receiving emails from it, send an email to HomotopyTy= peTheory+unsubscribe@googlegroups.com.
For more options, = visit https://gro= ups.google.com/d/optout.
<= br class=3D"">

--
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.
--Apple-Mail=_293D0AF5-E8AF-46EA-9A05-7BE46C55978B--