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 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 mathematician rather than computer scientist. So, it would be wonderful for me to use topological language and maybe topological intuition when I am programming in Isabelle/HOL (simple 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 Shulman () escribió: > 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é 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öf type theory with 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. > > > > HoTT is traditionally developed in CiC, whereas UniMath is > traditionally developed in the Martin-Löf 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é 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.