*[HoTT] Characteristic Classes for Types@ 2018-09-27 13:10 Juan Ospina2018-09-28 0:38 ` [HoTT] " Ali Caglayan 2018-09-28 5:59 ` [HoTT] the weak infinite groupoid in Simple Type Theory José Manuel Rodriguez Caballero 0 siblings, 2 replies; 12+ messages in thread From: Juan Ospina @ 2018-09-27 13:10 UTC (permalink / raw) To: Homotopy Type Theory [-- Attachment #1.1: Type: text/plain, Size: 1001 bytes --] Recently, there was a post about the Euler characteristic of a type and other post about Hodge structure of a type. Then my questions are: 1) It is possible to construct characteristic classes (Wu, Stiefel-Whitney, Chern, Pontryagin classes) for an arbitrary type in HoTT? 2) It is possible to construct singular cohomology for a type and the corresponding Steenrod operations? 3) It is possible to construct an Aityah-Singer index theorem for an arbitrary type (a type fibered with other type). 4) It is possible to construct integrality theores for the characteristic numbers of an arbitrary fibered type? Many thanks. Juan Ospina Medellín, Colombia -- 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. [-- Attachment #1.2: Type: text/html, Size: 1375 bytes --] ^ permalink raw reply [flat|nested] 12+ messages in thread

*[HoTT] Re: Characteristic Classes for Types2018-09-27 13:10 [HoTT] Characteristic Classes for Types Juan Ospina@ 2018-09-28 0:38 ` Ali Caglayan2018-09-28 1:00 ` Juan Ospina ` (2 more replies) 2018-09-28 5:59 ` [HoTT] the weak infinite groupoid in Simple Type Theory José Manuel Rodriguez Caballero 1 sibling, 3 replies; 12+ messages in thread From: Ali Caglayan @ 2018-09-28 0:38 UTC (permalink / raw) To: Homotopy Type Theory [-- Attachment #1.1: Type: text/plain, Size: 4589 bytes --] 1. This could be possible once a vector bundle has been fully defined. The idea behind characteristic classes is to classify certain vector bundles with cohomology. This however may be a bit in the future as, for example, grassmannians have not yet been defined. Also orthogonal groups are not yet defined. So it is impossible to say right now if this can be done but it seems likely. 2. Cohomology in HoTT is not by default singular cohomology like in algebraic topology. In HoTT we take the definition of cohomology to be the (truncated) set of maps to an Eilenberg-Maclane space. Concering cohomology operations, this should definitely be possible. Literature on cohomology has come out in the last few years so expect more to be written about it. 3. Atiyah-Singer would need quite a lot of work, not to mention the fact it involves differential structure. Which at the moment it is expected that differential cohesive HoTT may be able to tackle such a theorem. HoTT on it's own is quite good at talking about purely homotopical structure. This is an important point because many topological/manifoldy theorems are not necesserily homotopical in nature. They may depend on extra structure that HoTT cannot really describe adequately yet. Take for example Riemann-Roch which can be considered a special case of Atiyah-Singer. It would need a good amount of algebraic geometry to be defined and/or proven in order to state the theorem. Which is unliekly to come around in the next few years. This doesn't mean it couldn't happen. Just to show you how underdeveloped cohomology in HoTT is at the moment, an "elementary" theorem of algebraic topology, the Hurewicz theorem, has not been proven yet. Though I believe it will be tackled soon. Types are not topological spaces, they are more literally homotopy types. This is why I personally, found "the Hodge structure of a type" to be not within our current viewpoint although Steve Awodey's point about the speed of the development of HoTT has been considered. And one final thing: One of the reasons algebraic topologists are exicited about using and developing HoTT is that it gives a synthetic foundation to many "purely homotopical" ideas used in algebraic topology that have proofs and constructions relient on outside ideas or formalisms. This isn't necesserily a bad thing (look at cobordisms in stable homotopy) however some simpler areas of the subject should be able to hold their own. (As I understand). Therefore it stands to reason that it is unlikely that HoTT will bring anything new to the table when it comes to the ideas you are talking about. HoTT essentially provides a synthetic way to reason about homotopy types, but it isn't an enlightening viewpoint for theorems not homotopic in nature. And really finally this time: Have a look around at what people are doing in HoTT at the moment. For example Floris van Doorn's thesis where spectral sequences for cohomology have been developed in HoTT and formalised in the Spectral library for the Lean proof assistant. The agda formalisation of HoTT also usually has a lot of the latest gadgets of snythetic homootpy theory. Which is a fascinating subject if I do say so myself, but it isn't algebraic topology. There is a massive intersection but don't take them to be the same thing. Anyway if you have read this for congratulations. Ali Caglayan On Thursday, 27 September 2018 14:10:09 UTC+1, Juan Ospina wrote: > > Recently, there was a post about the Euler characteristic of a type and > other post about Hodge structure of a type. Then my questions are: > > 1) It is possible to construct characteristic classes (Wu, > Stiefel-Whitney, Chern, Pontryagin classes) for an arbitrary type in > HoTT? > > 2) It is possible to construct singular cohomology for a type and the > corresponding Steenrod operations? > > 3) It is possible to construct an Aityah-Singer index theorem for an > arbitrary type (a type fibered with other type). > > 4) It is possible to construct integrality theores for the characteristic > numbers of an arbitrary fibered type? > > > Many thanks. > > Juan Ospina > Medellín, Colombia > > > -- 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. [-- Attachment #1.2: Type: text/html, Size: 5763 bytes --] ^ permalink raw reply [flat|nested] 12+ messages in thread

*[HoTT] Re: Characteristic Classes for Types2018-09-28 0:38 ` [HoTT] " Ali Caglayan@ 2018-09-28 1:00 ` Juan Ospina2018-09-28 1:04 ` Juan Ospina 2018-09-28 2:51 ` Michael Shulman 2 siblings, 0 replies; 12+ messages in thread From: Juan Ospina @ 2018-09-28 1:00 UTC (permalink / raw) To: Homotopy Type Theory [-- Attachment #1.1: Type: text/plain, Size: 5083 bytes --] Many thanks for your comments which are very instructive. Actually I am trying to understand anything in the Floris van Doorn's thesis, particularly the formalization in HoTT for the *Atiyah*-*Hirzebruch spectral* sequence and the *Leray*-*Serre spectral* sequence. On Thursday, September 27, 2018 at 7:38:09 PM UTC-5, Ali Caglayan wrote: > > 1. This could be possible once a vector bundle has been fully defined. The > idea behind characteristic classes is to classify certain vector bundles > with cohomology. This however may be a bit in the future as, for example, > grassmannians have not yet been defined. Also orthogonal groups are not yet > defined. So it is impossible to say right now if this can be done but it > seems likely. > > 2. Cohomology in HoTT is not by default singular cohomology like in > algebraic topology. In HoTT we take the definition of cohomology to be the > (truncated) set of maps to an Eilenberg-Maclane space. Concering cohomology > operations, this should definitely be possible. Literature on cohomology > has come out in the last few years so expect more to be written about it. > > 3. Atiyah-Singer would need quite a lot of work, not to mention the fact > it involves differential structure. Which at the moment it is expected that > differential cohesive HoTT may be able to tackle such a theorem. HoTT on > it's own is quite good at talking about purely homotopical structure. This > is an important point because many topological/manifoldy theorems are not > necesserily homotopical in nature. They may depend on extra structure that > HoTT cannot really describe adequately yet. Take for example Riemann-Roch > which can be considered a special case of Atiyah-Singer. It would need a > good amount of algebraic geometry to be defined and/or proven in order to > state the theorem. Which is unliekly to come around in the next few years. > This doesn't mean it couldn't happen. > > Just to show you how underdeveloped cohomology in HoTT is at the moment, > an "elementary" theorem of algebraic topology, the Hurewicz theorem, has > not been proven yet. Though I believe it will be tackled soon. > > Types are not topological spaces, they are more literally homotopy types. > This is why I personally, found "the Hodge structure of a type" to be not > within our current viewpoint although Steve Awodey's point about the speed > of the development of HoTT has been considered. > > And one final thing: One of the reasons algebraic topologists are exicited > about using and developing HoTT is that it gives a synthetic foundation to > many "purely homotopical" ideas used in algebraic topology that have proofs > and constructions relient on outside ideas or formalisms. This isn't > necesserily a bad thing (look at cobordisms in stable homotopy) however > some simpler areas of the subject should be able to hold their own. (As I > understand). > > Therefore it stands to reason that it is unlikely that HoTT will bring > anything new to the table when it comes to the ideas you are talking about. > HoTT essentially provides a synthetic way to reason about homotopy types, > but it isn't an enlightening viewpoint for theorems not homotopic in nature. > > And really finally this time: Have a look around at what people are doing > in HoTT at the moment. For example Floris van Doorn's thesis where spectral > sequences for cohomology have been developed in HoTT and formalised in the > Spectral library for the Lean proof assistant. The agda formalisation of > HoTT also usually has a lot of the latest gadgets of snythetic homootpy > theory. Which is a fascinating subject if I do say so myself, but it isn't > algebraic topology. There is a massive intersection but don't take them to > be the same thing. > > Anyway if you have read this for congratulations. > > Ali Caglayan > > On Thursday, 27 September 2018 14:10:09 UTC+1, Juan Ospina wrote: >> >> Recently, there was a post about the Euler characteristic of a type and >> other post about Hodge structure of a type. Then my questions are: >> >> 1) It is possible to construct characteristic classes (Wu, >> Stiefel-Whitney, Chern, Pontryagin classes) for an arbitrary type in >> HoTT? >> >> 2) It is possible to construct singular cohomology for a type and the >> corresponding Steenrod operations? >> >> 3) It is possible to construct an Aityah-Singer index theorem for an >> arbitrary type (a type fibered with other type). >> >> 4) It is possible to construct integrality theores for the characteristic >> numbers of an arbitrary fibered type? >> >> >> Many thanks. >> >> Juan Ospina >> Medellín, Colombia >> >> >> -- 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. [-- Attachment #1.2: Type: text/html, Size: 6306 bytes --] ^ permalink raw reply [flat|nested] 12+ messages in thread

*[HoTT] Re: Characteristic Classes for Types2018-09-28 0:38 ` [HoTT] " Ali Caglayan 2018-09-28 1:00 ` Juan Ospina@ 2018-09-28 1:04 ` Juan Ospina2018-09-28 2:51 ` Michael Shulman 2 siblings, 0 replies; 12+ messages in thread From: Juan Ospina @ 2018-09-28 1:04 UTC (permalink / raw) To: Homotopy Type Theory [-- Attachment #1.1: Type: text/plain, Size: 585 bytes --] Ali, many thanks for your comments which are very instructive. Actually I am trying to understand anything in the Floris van Doorn's thesis, particularly the formalization in HoTT for the *Atiyah*-*Hirzebruch spectral* sequence and the *Leray*-*Serre spectral* sequence. > -- 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. [-- Attachment #1.2: Type: text/html, Size: 1022 bytes --] ^ permalink raw reply [flat|nested] 12+ messages in thread

*Re: [HoTT] Re: Characteristic Classes for Types2018-09-28 0:38 ` [HoTT] " Ali Caglayan 2018-09-28 1:00 ` Juan Ospina 2018-09-28 1:04 ` Juan Ospina@ 2018-09-28 2:51 ` Michael Shulman2 siblings, 0 replies; 12+ messages in thread From: Michael Shulman @ 2018-09-28 2:51 UTC (permalink / raw) To: Ali Caglayan;+Cc:HomotopyTypeTheory The Hurewicz theorem is actually a theorem about *homology*, which is indeed undeveloped in HoTT. Cohomology is much better understood. The questions you're asking *do* have a significant homotopical nature, and so I think it *is* reasonably likely that the synthetic approach -- especially augmented with cohesion -- will have something interesting to contribute to them. But not yet. I think really the best answer to questions like this is Ali's last paragraph: start by reading up on the state of the art. You'll get a much better sense that way of what is known, what sort of things are easy, what sort of things are hard, and what sort of things are likely to be doable soon. (If state-of-the-art papers are hard to understand, then start with earlier stuff instead, like the HoTT Book.) On Thu, Sep 27, 2018 at 5:38 PM Ali Caglayan <alizter@gmail.com> wrote: > > 1. This could be possible once a vector bundle has been fully defined. The idea behind characteristic classes is to classify certain vector bundles with cohomology. This however may be a bit in the future as, for example, grassmannians have not yet been defined. Also orthogonal groups are not yet defined. So it is impossible to say right now if this can be done but it seems likely. > > 2. Cohomology in HoTT is not by default singular cohomology like in algebraic topology. In HoTT we take the definition of cohomology to be the (truncated) set of maps to an Eilenberg-Maclane space. Concering cohomology operations, this should definitely be possible. Literature on cohomology has come out in the last few years so expect more to be written about it. > > 3. Atiyah-Singer would need quite a lot of work, not to mention the fact it involves differential structure. Which at the moment it is expected that differential cohesive HoTT may be able to tackle such a theorem. HoTT on it's own is quite good at talking about purely homotopical structure. This is an important point because many topological/manifoldy theorems are not necesserily homotopical in nature. They may depend on extra structure that HoTT cannot really describe adequately yet. Take for example Riemann-Roch which can be considered a special case of Atiyah-Singer. It would need a good amount of algebraic geometry to be defined and/or proven in order to state the theorem. Which is unliekly to come around in the next few years. This doesn't mean it couldn't happen. > > Just to show you how underdeveloped cohomology in HoTT is at the moment, an "elementary" theorem of algebraic topology, the Hurewicz theorem, has not been proven yet. Though I believe it will be tackled soon. > > Types are not topological spaces, they are more literally homotopy types. This is why I personally, found "the Hodge structure of a type" to be not within our current viewpoint although Steve Awodey's point about the speed of the development of HoTT has been considered. > > And one final thing: One of the reasons algebraic topologists are exicited about using and developing HoTT is that it gives a synthetic foundation to many "purely homotopical" ideas used in algebraic topology that have proofs and constructions relient on outside ideas or formalisms. This isn't necesserily a bad thing (look at cobordisms in stable homotopy) however some simpler areas of the subject should be able to hold their own. (As I understand). > > Therefore it stands to reason that it is unlikely that HoTT will bring anything new to the table when it comes to the ideas you are talking about. HoTT essentially provides a synthetic way to reason about homotopy types, but it isn't an enlightening viewpoint for theorems not homotopic in nature. > > And really finally this time: Have a look around at what people are doing in HoTT at the moment. For example Floris van Doorn's thesis where spectral sequences for cohomology have been developed in HoTT and formalised in the Spectral library for the Lean proof assistant. The agda formalisation of HoTT also usually has a lot of the latest gadgets of snythetic homootpy theory. Which is a fascinating subject if I do say so myself, but it isn't algebraic topology. There is a massive intersection but don't take them to be the same thing. > > Anyway if you have read this for congratulations. > > Ali Caglayan > > On Thursday, 27 September 2018 14:10:09 UTC+1, Juan Ospina wrote: >> >> Recently, there was a post about the Euler characteristic of a type and other post about Hodge structure of a type. Then my questions are: >> >> 1) It is possible to construct characteristic classes (Wu, Stiefel-Whitney, Chern, Pontryagin classes) for an arbitrary type in HoTT? >> >> 2) It is possible to construct singular cohomology for a type and the corresponding Steenrod operations? >> >> 3) It is possible to construct an Aityah-Singer index theorem for an arbitrary type (a type fibered with other type). >> >> 4) It is possible to construct integrality theores for the characteristic numbers of an arbitrary fibered type? >> >> >> Many thanks. >> >> Juan Ospina >> Medellín, Colombia >> >> > -- > 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. ^ permalink raw reply [flat|nested] 12+ messages in thread

*[HoTT] the weak infinite groupoid in Simple Type Theory2018-09-27 13:10 [HoTT] Characteristic Classes for Types Juan Ospina 2018-09-28 0:38 ` [HoTT] " Ali Caglayan@ 2018-09-28 5:59 ` José Manuel Rodriguez Caballero2018-09-28 19:21 ` Michael Shulman 1 sibling, 1 reply; 12+ messages in thread From: José Manuel Rodriguez Caballero @ 2018-09-28 5:59 UTC (permalink / raw) To: HomotopyTypeTheory;+Cc:Joshua Chen [-- Attachment #1: Type: text/plain, Size: 1274 bytes --] 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. [-- Attachment #2: Type: text/html, Size: 1903 bytes --] ^ permalink raw reply [flat|nested] 12+ messages in thread

*Re: [HoTT] the weak infinite groupoid in Simple Type Theory2018-09-28 5:59 ` [HoTT] the weak infinite groupoid in Simple Type Theory José Manuel Rodriguez Caballero@ 2018-09-28 19:21 ` Michael Shulman2018-09-28 20:27 ` José Manuel Rodriguez Caballero 0 siblings, 1 reply; 12+ messages in thread From: Michael Shulman @ 2018-09-28 19:21 UTC (permalink / raw) To: josephcmac;+Cc:HomotopyTypeTheory, joshua.chen 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 <josephcmac@gmail.com> 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. ^ permalink raw reply [flat|nested] 12+ messages in thread

*Re: [HoTT] the weak infinite groupoid in Simple Type Theory2018-09-28 19:21 ` Michael Shulman@ 2018-09-28 20:27 ` José Manuel Rodriguez Caballero2018-10-01 14:43 ` Michael Shulman 0 siblings, 1 reply; 12+ messages in thread From: José Manuel Rodriguez Caballero @ 2018-09-28 20:27 UTC (permalink / raw) To: HomotopyTypeTheory;+Cc:Joshua Chen [-- Attachment #1: Type: text/plain, Size: 5850 bytes --] 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 (<shulman@sandiego.edu>) 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 > <josephcmac@gmail.com> 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. [-- Attachment #2: Type: text/html, Size: 7333 bytes --] ^ permalink raw reply [flat|nested] 12+ messages in thread

*Re: [HoTT] the weak infinite groupoid in Simple Type Theory2018-09-28 20:27 ` José Manuel Rodriguez Caballero@ 2018-10-01 14:43 ` Michael Shulman2018-10-01 14:53 ` Steve Awodey 0 siblings, 1 reply; 12+ messages in thread From: Michael Shulman @ 2018-10-01 14:43 UTC (permalink / raw) To: josephcmac;+Cc:HomotopyTypeTheory, joshua.chen 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é Manuel Rodriguez Caballero <josephcmac@gmail.com> 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 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 (<shulman@sandiego.edu>) 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 >> <josephcmac@gmail.com> 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. -- 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. ^ permalink raw reply [flat|nested] 12+ messages in thread

*Re: [HoTT] the weak infinite groupoid in Simple Type Theory2018-10-01 14:43 ` Michael Shulman@ 2018-10-01 14:53 ` Steve Awodey2018-10-01 23:14 ` José Manuel Rodriguez Caballero 0 siblings, 1 reply; 12+ messages in thread From: Steve Awodey @ 2018-10-01 14:53 UTC (permalink / raw) To: Michael Shulman;+Cc:josephcmac, HomotopyTypeTheory, joshua.chen [-- Attachment #1: Type: text/plain, Size: 7798 bytes --] 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 <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 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é Manuel Rodriguez Caballero > <josephcmac@gmail.com> 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 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 (<shulman@sandiego.edu>) 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 >>> <josephcmac@gmail.com> 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. > > -- > 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. [-- Attachment #2: Type: text/html, Size: 10547 bytes --] ^ permalink raw reply [flat|nested] 12+ messages in thread

*Re: [HoTT] the weak infinite groupoid in Simple Type Theory2018-10-01 14:53 ` Steve Awodey@ 2018-10-01 23:14 ` José Manuel Rodriguez Caballero2018-10-02 16:20 ` Michael Shulman 0 siblings, 1 reply; 12+ messages in thread From: José Manuel Rodriguez Caballero @ 2018-10-01 23:14 UTC (permalink / raw) To: HomotopyTypeTheory;+Cc:Joshua Chen [-- Attachment #1: Type: text/plain, Size: 8667 bytes --] > > 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 = n" and "finite S" shows "card {p. p permutes S} = fact n" in HOL/Library/Permutations.thy is a truncation of the following theorem due to Voevodsky Theorem weqfromweqstntostn ( n : nat ) : ( (⟦n⟧) ≃ (⟦n⟧) ) ≃ ⟦factorial n⟧. which can be found here: https://github.com/UniMath/UniMath/blob/master/UniMath/Combinatorics/StandardFiniteSets.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é M. El lun., 1 oct. 2018 a las 10:53, Steve Awodey (<awodey@cmu.edu>) escribió: > 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 <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 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é Manuel Rodriguez Caballero > <josephcmac@gmail.com> 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 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 (<shulman@sandiego.edu>) > 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 > <josephcmac@gmail.com> 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. > > > -- > 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. [-- Attachment #2: Type: text/html, Size: 11243 bytes --] ^ permalink raw reply [flat|nested] 12+ messages in thread

*2018-10-01 23:14 ` José Manuel Rodriguez CaballeroRe: [HoTT] the weak infinite groupoid in Simple Type Theory@ 2018-10-02 16:20 ` Michael Shulman0 siblings, 0 replies; 12+ messages in thread From: Michael Shulman @ 2018-10-02 16:20 UTC (permalink / raw) To: josephcmac;+Cc:HomotopyTypeTheory, joshua.chen These lemmas are just standard facts of set-level mathematics; nothing fancy or univalent is required to formalize them in HoTT. If you replace the equivalences by equalities, then that would be using univalence. On Mon, Oct 1, 2018 at 4:15 PM José Manuel Rodriguez Caballero <josephcmac@gmail.com> wrote: >> >> 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 = n" > and "finite S" > shows "card {p. p permutes S} = fact n" > > in HOL/Library/Permutations.thy > > is a truncation of the following theorem due to Voevodsky > > Theorem weqfromweqstntostn ( n : nat ) : ( (⟦n⟧) ≃ (⟦n⟧) ) ≃ ⟦factorial n⟧. > > which can be found here: https://github.com/UniMath/UniMath/blob/master/UniMath/Combinatorics/StandardFiniteSets.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é M. > > > El lun., 1 oct. 2018 a las 10:53, Steve Awodey (<awodey@cmu.edu>) escribió: >> >> 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 <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 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é Manuel Rodriguez Caballero >> <josephcmac@gmail.com> 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 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 (<shulman@sandiego.edu>) 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 >> <josephcmac@gmail.com> 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. >> >> >> -- >> 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. ^ permalink raw reply [flat|nested] 12+ messages in thread

end of thread, other threads:[~2018-10-02 16:20 UTC | newest]Thread overview:12+ messages (download: mbox.gz / follow: Atom feed) -- links below jump to the message on this page -- 2018-09-27 13:10 [HoTT] Characteristic Classes for Types Juan Ospina 2018-09-28 0:38 ` [HoTT] " Ali Caglayan 2018-09-28 1:00 ` Juan Ospina 2018-09-28 1:04 ` Juan Ospina 2018-09-28 2:51 ` Michael Shulman 2018-09-28 5:59 ` [HoTT] the weak infinite groupoid in Simple Type Theory José Manuel Rodriguez Caballero 2018-09-28 19:21 ` Michael Shulman 2018-09-28 20:27 ` José Manuel Rodriguez Caballero 2018-10-01 14:43 ` Michael Shulman 2018-10-01 14:53 ` Steve Awodey 2018-10-01 23:14 ` José Manuel Rodriguez Caballero 2018-10-02 16:20 ` Michael Shulman

This is a public inbox, see mirroring instructions for how to clone and mirror all data and code used for this inbox; as well as URLs for NNTP newsgroup(s).