[HoTT] Characteristic Classes for Types

[HoTT] Characteristic Classes for Types

[Juan Ospina]

[-- 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 --]

[HoTT] Re: Characteristic Classes for Types

[Ali Caglayan]

[-- 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 --]

[HoTT] Re: Characteristic Classes for Types

[Juan Ospina]

[-- 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 --]

[HoTT] Re: Characteristic Classes for Types

[Juan Ospina]

[-- 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 --]

Re: [HoTT] Re: Characteristic Classes for Types

[Michael Shulman]

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.

[HoTT] the weak infinite groupoid in Simple Type Theory

[José Manuel Rodriguez Caballero]

[-- 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 --]

Re: [HoTT] the weak infinite groupoid in Simple Type Theory

[Michael Shulman]

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.

Re: [HoTT] the weak infinite groupoid in Simple Type Theory

[José Manuel Rodriguez Caballero]

[-- 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 --]

Re: [HoTT] the weak infinite groupoid in Simple Type Theory

[Michael Shulman]

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.

Re: [HoTT] the weak infinite groupoid in Simple Type Theory

[Steve Awodey]

[-- 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 --]

Re: [HoTT] the weak infinite groupoid in Simple Type Theory

[José Manuel Rodriguez Caballero]

[-- 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 --]

Re: [HoTT] the weak infinite groupoid in Simple Type Theory

[Michael Shulman]

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.