What is UF, what is HoTT and what is a univalent type theory?

What is UF, what is HoTT and what is a univalent type theory?

[Martin Escardo]

What is UF (univalent foundations), what is HoTT and what is a
univalent type theory (UTT)?

The three of them start with a Martin-Lof type theory.

(However, any claim here about UF is just an unjustified claim, and at
best a guess, because I have never seen a (precise or even imprecise)
defininition of what UF should be. Whatever Vladimir replies about UF
is to be taken as correct by definition, and as an answer of what he
defines UF to be.)

By a Martin-Lof type theory I will mean any dependent type theory with
an identity-type former, and not necessarily with a universe.

To formulate the univalence axiom, we need a Martin-Lof type theory
with a universe U (or many universes if we wish).

The reason is that the univalence axiom is an axiom about (the
identity type of) the type U.

However, we have that UF, HoTT and UTT start much before we have a
universe U and we postulate the univalence axiom for it.

It starts by defining the notions of -1-type (proposition), 0-type
(set), 1-type (groupoid), and so on. And then, with this, defining the
notions of equivalence, embedding, surjection. And so on again.

In this sense, UF/HoTT/UTT is about, to begin with, giving the right
definitions for working in MLTT, even before the univalence axiom is
considered.

Much of mathematics takes place at the 0-level (sets). For this kind
of mathematics rendered in type theory, function extensionality and
propositional extensionality are essential.

Each of them is a particular case of the univalence axiom, as
discovered by Vladimir.

But then, for example, we have categories. The type of categories is
not a set. It is for types such as this that the univalence axiom is
used beyond its two particular cases discussed above (function
extensionality and propositional extensionality).

And what about higher-inductive types (HIT's)? Well, modulo size
considerations, many of them begin to exist with the univalence axiom
alone.  This is the case, for instance, for propositional truncation,
quotients and the circle (as per discussion in this list in the past).

We can now do a lot more of mathematics in Martin-Lof type theory from
what we have learned from UF/HoTT/UTT. Very often we need only
function extensionality and propositional extensionality, as two
particular cases of univalence, including the possibility to form
quotients.

The point, which perhaps is not made sufficiently explicit in the Book,
is that only when we climb to categories and the like is that the full
force of the univalence axiom is needed.

This is where I come from.

But a number of people come from another direction: MLTT plus
univalence and higher inductive types can be used as a language for
synthetic homotopy (and perhaps infty-toposes). This is nice, and I
like this very much. But it is a completely different perspective to
the subject, not necessarily the primary one.

Let me then come to the last of the three questions. What is UTT
(univalent type theory)? As I conceive it:

     It is any Martin-Lof type theory that is compatible with the idea
     that equality/equivalence, as rendered by the identity type, is,
     in general, structure rather than merely a property.

The subtlety (again articulated by Vladimir) is that "e is an equality
of x and y" is always supposed to be a property of the triple (e,x,y)
(i.e. a -1-type), but, on the other hand, there may be another
equality e' of x and y which is not equal to e, so that "x is equal to
y" may be a proposition in the "proposition as types" sense, but not
in the usual sense of a proposition as a truth value. (The usual sense
is captured by the notion of -1-type, as you know.) In any case, in
order to understand univalent type theory, it is essential to
understand the distinction of proposition as types versus proposition
as truth values, and make use of both in a subtle way, particularly
when it comes to the identity type.

Intensional Martin-Lof type theory is a univalent type theory, in this
sense. It is prepared to allow for such distinctions, before the
univalence axiom is considered. Importantly, MLTT allows the
formulation of the univalence axiom.

A competing univalent type theory is cubicaltt, in which such
distinctions are not only allowed but made good. The difference with
HoTT is that in HoTT such distinctions are merely axiomatized. In
cubicaltt they just hold. We can appreciate this before we even begin
to talk about computation, which cubicaltt also makes good.

Martin

Re: What is UF, what is HoTT and what is a univalent type theory?

[Andrew Polonsky]

[-- Attachment #1.1: Type: text/plain, Size: 813 bytes --]


>
> Let me then come to the last of the three questions. What is UTT 
> (univalent type theory)? As I conceive it: 
>
>      It is any Martin-Lof type theory that is compatible with the idea 
>      that equality/equivalence, as rendered by the identity type, is, 
>      in general, structure rather than merely a property. 
>

I find this definition somewhat puzzling.  Cubicaltt is certainly 
compatible with the idea that equality is equivalence.  But its path type 
seems to be a very different concept compared to Martin-Lof identity type.

What is a Martin-Lof type theory anyway?  Are type systems based on untyped 
conversion (eg. Coq) Martin-Lof type theories?  Are type theories with a 
different notion of equality (eg. observational or cubical type theories) 
also Martin-Lof type theories?

Andrew

[-- Attachment #1.2: Type: text/html, Size: 1052 bytes --]

Re: [HoTT] Re: What is UF, what is HoTT and what is a univalent type theory?

[Vladimir Voevodsky]

[-- Attachment #1.1: Type: text/plain, Size: 2776 bytes --]

The original approach to the UF in 2005-2006 used homotopy lambda calculus, the type theory that I tried to construct, that did not have Martin-Lof identity types. In fact, the idea of having many elements of the identity type in the empty context is against Martin-Lof’s philosophy. MLTT in the form of the CIC just happened to be both implemented in Coq and not inconsistent with the UA opening a way for practical formalization of mathematics in the UF style. This led to the UniMath and a number of HoTT libraries and gave us a great platform for experiment.

However the original philosophy of MLTT and the original philosophy of UF are different and our use of MLTT for UF is in a sense an abuse of the MLTT as Per himself politely mentioned a number of times.

The current work on the development of new type theories led by Bob Harper, Thorsten Altenkirch and Thierry Coquand (and probably others whom I have forgotten to mention) moves us towards a native formal system for the UF but we don’t yet have such a system. We are also isolated from many and many mathematicians who are trying to find a way to express ideas that in my opinion are most naturally expressed in the UF in various theories formulated inside the set theory.

It is, currently, not the best time for the attempts to summarize the theory. We are far having it and I see no other tactic then to move forward slowly and invest into attracting mathematicians to what we do.

Vladimir.





> On Jun 3, 2016, at 2:53 PM, Andrew Polonsky <andrew....@gmail.com> wrote:
> 
> Let me then come to the last of the three questions. What is UTT
> (univalent type theory)? As I conceive it:
> 
>      It is any Martin-Lof type theory that is compatible with the idea
>      that equality/equivalence, as rendered by the identity type, is,
>      in general, structure rather than merely a property.
> 
> I find this definition somewhat puzzling.  Cubicaltt is certainly compatible with the idea that equality is equivalence.  But its path type seems to be a very different concept compared to Martin-Lof identity type.
> 
> What is a Martin-Lof type theory anyway?  Are type systems based on untyped conversion (eg. Coq) Martin-Lof type theories?  Are type theories with a different notion of equality (eg. observational or cubical type theories) also Martin-Lof type theories?
> 
> Andrew
> 
> --
> 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 HomotopyTypeThe...@googlegroups.com <mailto:HomotopyTypeThe...@googlegroups.com>.
> For more options, visit https://groups.google.com/d/optout <https://groups.google.com/d/optout>.


[-- Attachment #1.2: Type: text/html, Size: 4117 bytes --]

[-- Attachment #2: Message signed with OpenPGP using GPGMail --]
[-- Type: application/pgp-signature, Size: 507 bytes --]

Re: [HoTT] Re: What is UF, what is HoTT and what is a univalent type theory?

[Andrew Polonsky]

[-- Attachment #1: Type: text/plain, Size: 477 bytes --]

Dear Vladimir,

We are also isolated from many and many mathematicians who are trying to
> find a way to express ideas that in my opinion are most naturally expressed
> in the UF in various theories formulated inside the set theory.
>

In this paragraph, are you referring to what Martin called "synthetic
homotopy theory/infinity-toposes" branch of the HoTT community, or to a
disparate body of mathematical research with different objectives?

Greetings,
Andrew

[-- Attachment #2: Type: text/html, Size: 789 bytes --]

Re: [HoTT] Re: What is UF, what is HoTT and what is a univalent type theory?

[Vladimir Voevodsky]

[-- Attachment #1.1: Type: text/plain, Size: 1312 bytes --]

Certainly not to the synthetic homotopy theory branch with which we communicate all the time.

I refer to mathematicians who do not know type theory and want to have a convenient language of working with what we would call structures on types of higher h-level.

For example, there are people like that in the geometric representation theory.

They don’t take us seriously so far because we can not define (infty,1)-categories. As soon as we find a language that can be used to define them and work with them directly without going through sets they will all start to turn their heads in our direction.

And this is a necessary pre-condition for talking seriously about the UF as a new foundation of mathematics.

Vladimir.





> On Jun 3, 2016, at 5:12 PM, Andrew Polonsky <andrew....@gmail.com> wrote:
> 
> Dear Vladimir,
> 
> We are also isolated from many and many mathematicians who are trying to find a way to express ideas that in my opinion are most naturally expressed in the UF in various theories formulated inside the set theory.
> 
> In this paragraph, are you referring to what Martin called "synthetic homotopy theory/infinity-toposes" branch of the HoTT community, or to a disparate body of mathematical research with different objectives?
> 
> Greetings,
> Andrew


[-- Attachment #1.2: Type: text/html, Size: 2538 bytes --]

[-- Attachment #2: Message signed with OpenPGP using GPGMail --]
[-- Type: application/pgp-signature, Size: 507 bytes --]

Re: [HoTT] Re: What is UF, what is HoTT and what is a univalent type theory?

[andré hirschowitz]

[-- Attachment #1: Type: text/plain, Size: 1010 bytes --]

Hi,

2016-06-03 21:29 GMT+02:00 Vladimir Voevodsky <vlad...@ias.edu>:

> They don’t take us seriously so far because we can not define
> (infty,1)-categories. As soon as we find a language that can be used to
> define them and work with them directly without going through sets they
> will all start to turn their heads in our direction.


I can believe it is reachable to define "their" notion(s) of infty-cats
within UF "through sets". Are you claiming for an "equivalent" definition
"without sets"? Or for the "right"  type-theoretic counterpart of "their"
notion(s)?
And could you further say something about what you would accept for
"equivalent" or for "right"?

Anyway, why would "they" turn their heads? They have no need, do they?

By the way, I suspect the definition you claim for would be formalized, and
it would probably be quite involved. Except if you require (and prove) a
characteristic property, it would be a hard (human) task to check that it
is reasonable.

ah

[-- Attachment #2: Type: text/html, Size: 1481 bytes --]

Re: [HoTT] Re: What is UF, what is HoTT and what is a univalent type theory?

[Vladimir Voevodsky]

[-- Attachment #1.1: Type: text/plain, Size: 2228 bytes --]

Hi Andre,

1. Are you claiming for an "equivalent" definition "without sets"? Or for the "right"  type-theoretic counterpart of "their" notion(s)?

For the “right” type-theoretic counterpart of “their” notion. To make it equivalent (to show that there exists, in the weak sense, an equivalence) to the one constructed through sets one would have to add axiom of choice in the form that says that for any surjection T -> X where X is an h-set there exists, in the weak sense, a section X -> T. Maybe more axioms will be required but it is possible that this one will suffice.

2. And could you further say something about what you would accept for "equivalent" or for "right”?

For the “right” I will accept a collection of theorems, including construction of examples, that shows that these objects behave in the way expected from (inty,1)-categories.

3. By the way, I suspect the definition you claim for would be formalized, and it would probably be quite involved.

It is very easy to formalize, for example in UniMath, the concept of a quasi-category.

Vladimir.






> On Jun 4, 2016, at 1:05 AM, andré hirschowitz <a...@unice.fr> wrote:
> 
> Hi,
> 
> 2016-06-03 21:29 GMT+02:00 Vladimir Voevodsky <vlad...@ias.edu <mailto:vlad...@ias.edu>>:
> They don’t take us seriously so far because we can not define (infty,1)-categories. As soon as we find a language that can be used to define them and work with them directly without going through sets they will all start to turn their heads in our direction.
> 
> I can believe it is reachable to define "their" notion(s) of infty-cats  within UF "through sets". Are you claiming for an "equivalent" definition "without sets"? Or for the "right"  type-theoretic counterpart of "their" notion(s)?
> And could you further say something about what you would accept for "equivalent" or for "right"?
> 
> Anyway, why would "they" turn their heads? They have no need, do they?
> 
> By the way, I suspect the definition you claim for would be formalized, and it would probably be quite involved. Except if you require (and prove) a characteristic property, it would be a hard (human) task to check that it is reasonable.
> 
> ah


[-- Attachment #1.2: Type: text/html, Size: 3694 bytes --]

[-- Attachment #2: Message signed with OpenPGP using GPGMail --]
[-- Type: application/pgp-signature, Size: 507 bytes --]

Re: [HoTT] Re: What is UF, what is HoTT and what is a univalent type theory?

[andré hirschowitz]

[-- Attachment #1: Type: text/plain, Size: 453 bytes --]

Thanks!

2016-06-04 10:38 GMT+02:00 Vladimir Voevodsky <vlad...@ias.edu>:

> It is very easy to formalize, for example in UniMath, the concept of a
> quasi-category.
>

I now understand that you even accept such a "flattened" notion of
(oo, 1)-category. Great! So, since at least one (simple, standard)
definition is already there, what exactly is missing in your view for them
"all start to turn their heads in [y]our direction"?

andré

[-- Attachment #2: Type: text/html, Size: 889 bytes --]

Re: [HoTT] What is UF, what is HoTT and what is a univalent type theory?

[Vladimir Voevodsky]

[-- Attachment #1.1: Type: text/plain, Size: 731 bytes --]

I said that they will start to turn their heads when we get a direct definition of an (inty,1)-category, not a one that reduces this concept to sets.


> On Jun 4, 2016, at 12:56 PM, andré hirschowitz <a...@unice.fr> wrote:
> 
> Thanks!
> 
> 2016-06-04 10:38 GMT+02:00 Vladimir Voevodsky <vlad...@ias.edu <mailto:vlad...@ias.edu>>:
> It is very easy to formalize, for example in UniMath, the concept of a quasi-category.
> 
> I now understand that you even accept such a "flattened" notion of
> (oo, 1)-category. Great! So, since at least one (simple, standard) definition is already there, what exactly is missing in your view for them "all start to turn their heads in [y]our direction"?
> 
> andré
> 
> 
> 


[-- Attachment #1.2: Type: text/html, Size: 1746 bytes --]

[-- Attachment #2: Message signed with OpenPGP using GPGMail --]
[-- Type: application/pgp-signature, Size: 507 bytes --]

Re: [HoTT] Re: What is UF, what is HoTT and what is a univalent type theory?

[Urs Schreiber]

> They don’t take us seriously so far because we can not define
> (infty,1)-categories.

The good news is, without even having to define them, HoTT already is
the internal language of certain (infinity,1)-categories. Which ones
precisely depends on which axioms are added or omitted.

For instance a class of (infinity,1)-categories that geometric
representation theorists care about is neatly obtained in HoTT by just
adding a certain adjoint triple of modal operators (differential
cohesion) This yields a synthetic axiomatization of the homotopy
theory of D-modules and their representation theory, which is what is
mostly meant by "geometric representation theory".

This route is the homotopy version of Lawvere's seminal vision of all
mathematics taking place synthetically inside a suitable elementary
topos. It's slightly ironic that this route is not more popular.
Because over in the community of ordinary (i.e. non-type theoretic)
infinity-category theory, there is the nagging feeling that handling
all those incarnations of infinity categories as simplicial and n-fold
simplicial objects from the outside may be rather inefficient for
deriving results. In order to overcome this there is the work on
derivators and the work by Riehl-Verity.

A colleague of mine championing derivators praises the fact that they
offer him a formal way to verify the simplicial reasoning in work by
Lurie et al, which he finds intricate to the point of being
unverifiable to him. This certainly applies to other people, too.

To check this, you should do a survey among your colleagues whether or
not they think that Lurie actually gave a proof of the cobordism
hypothesis. Lurie gives an intriciate argument in terms of
infinity-categories modeled on simplicial set, and while I fully trust
that it is correct, it is true that it gets to the point of compexity
where it seems that checking the proof is not just a matter of
mchanically checking derivation steps, but requires extra ingenuity.

Now, HoTT, regarded as an internal language, shares with the concept
of derivators the potential to make much of this somewhat
messy-looking simplicial infinity-category theory become more
transparent and systematic, more mechanical. Therefore it might be
argued to be a little be backwards to try to force that messy
simplicial technology to realize itself inside HoTT. It might be
missing the golden opportunity to turn this around and use the
synthetic reasong.

There is now one person, Felix Wellen, working on formalizing some
first basics of geometric representation theory within differentially
cohesion HoTT. I think it's a topic with plenty of opportunity.

Best wishes,
urs

Re: [HoTT] Re: What is UF, what is HoTT and what is a univalent type theory?

[Vladimir Voevodsky]

[-- Attachment #1: Type: text/plain, Size: 3413 bytes --]

Dear Urs,

> For instance a class of (infinity,1)-categories that geometric
> representation theorists care about is neatly obtained in HoTT by just
> adding a certain adjoint triple of modal operators (differential
> cohesion)

this is a lie.

Geometric representation theorists care about the (infty,1)-categories that corresponds to different groups and to their interaction with each other. They care not about sitting inside one universal (infty,1)-category.

Vladimir.





> On Jun 4, 2016, at 9:11 AM, Urs Schreiber <urs.sc...@googlemail.com> wrote:
> 
>> They don’t take us seriously so far because we can not define
>> (infty,1)-categories.
> 
> The good news is, without even having to define them, HoTT already is
> the internal language of certain (infinity,1)-categories. Which ones
> precisely depends on which axioms are added or omitted.
> 
> For instance a class of (infinity,1)-categories that geometric
> representation theorists care about is neatly obtained in HoTT by just
> adding a certain adjoint triple of modal operators (differential
> cohesion) This yields a synthetic axiomatization of the homotopy
> theory of D-modules and their representation theory, which is what is
> mostly meant by "geometric representation theory".
> 
> This route is the homotopy version of Lawvere's seminal vision of all
> mathematics taking place synthetically inside a suitable elementary
> topos. It's slightly ironic that this route is not more popular.
> Because over in the community of ordinary (i.e. non-type theoretic)
> infinity-category theory, there is the nagging feeling that handling
> all those incarnations of infinity categories as simplicial and n-fold
> simplicial objects from the outside may be rather inefficient for
> deriving results. In order to overcome this there is the work on
> derivators and the work by Riehl-Verity.
> 
> A colleague of mine championing derivators praises the fact that they
> offer him a formal way to verify the simplicial reasoning in work by
> Lurie et al, which he finds intricate to the point of being
> unverifiable to him. This certainly applies to other people, too.
> 
> To check this, you should do a survey among your colleagues whether or
> not they think that Lurie actually gave a proof of the cobordism
> hypothesis. Lurie gives an intriciate argument in terms of
> infinity-categories modeled on simplicial set, and while I fully trust
> that it is correct, it is true that it gets to the point of compexity
> where it seems that checking the proof is not just a matter of
> mchanically checking derivation steps, but requires extra ingenuity.
> 
> Now, HoTT, regarded as an internal language, shares with the concept
> of derivators the potential to make much of this somewhat
> messy-looking simplicial infinity-category theory become more
> transparent and systematic, more mechanical. Therefore it might be
> argued to be a little be backwards to try to force that messy
> simplicial technology to realize itself inside HoTT. It might be
> missing the golden opportunity to turn this around and use the
> synthetic reasong.
> 
> There is now one person, Felix Wellen, working on formalizing some
> first basics of geometric representation theory within differentially
> cohesion HoTT. I think it's a topic with plenty of opportunity.
> 
> Best wishes,
> urs


[-- Attachment #2: Message signed with OpenPGP using GPGMail --]
[-- Type: application/pgp-signature, Size: 507 bytes --]

Re: [HoTT] Re: What is UF, what is HoTT and what is a univalent type theory?

[David Roberts]

[-- Attachment #1: Type: text/plain, Size: 4226 bytes --]

Dear Vladimir,

Please see Charles Rezk's work on globally equivariant homotopy theoretic
models of cohesion. It is not something out of Urs' imagination.

Also, if something is false, call it false, not a 'lie', and provide a
mathematical basis for such a statement.

Best regards,
David
On 6 Jun 2016 4:45 pm, "Vladimir Voevodsky" <vlad...@ias.edu> wrote:

> Dear Urs,
>
> > For instance a class of (infinity,1)-categories that geometric
> > representation theorists care about is neatly obtained in HoTT by just
> > adding a certain adjoint triple of modal operators (differential
> > cohesion)
>
> this is a lie.
>
> Geometric representation theorists care about the (infty,1)-categories
> that corresponds to different groups and to their interaction with each
> other. They care not about sitting inside one universal (infty,1)-category.
>
> Vladimir.
>
>
>
>
>
> > On Jun 4, 2016, at 9:11 AM, Urs Schreiber <urs.sc...@googlemail.com>
> wrote:
> >
> >> They don’t take us seriously so far because we can not define
> >> (infty,1)-categories.
> >
> > The good news is, without even having to define them, HoTT already is
> > the internal language of certain (infinity,1)-categories. Which ones
> > precisely depends on which axioms are added or omitted.
> >
> > For instance a class of (infinity,1)-categories that geometric
> > representation theorists care about is neatly obtained in HoTT by just
> > adding a certain adjoint triple of modal operators (differential
> > cohesion) This yields a synthetic axiomatization of the homotopy
> > theory of D-modules and their representation theory, which is what is
> > mostly meant by "geometric representation theory".
> >
> > This route is the homotopy version of Lawvere's seminal vision of all
> > mathematics taking place synthetically inside a suitable elementary
> > topos. It's slightly ironic that this route is not more popular.
> > Because over in the community of ordinary (i.e. non-type theoretic)
> > infinity-category theory, there is the nagging feeling that handling
> > all those incarnations of infinity categories as simplicial and n-fold
> > simplicial objects from the outside may be rather inefficient for
> > deriving results. In order to overcome this there is the work on
> > derivators and the work by Riehl-Verity.
> >
> > A colleague of mine championing derivators praises the fact that they
> > offer him a formal way to verify the simplicial reasoning in work by
> > Lurie et al, which he finds intricate to the point of being
> > unverifiable to him. This certainly applies to other people, too.
> >
> > To check this, you should do a survey among your colleagues whether or
> > not they think that Lurie actually gave a proof of the cobordism
> > hypothesis. Lurie gives an intriciate argument in terms of
> > infinity-categories modeled on simplicial set, and while I fully trust
> > that it is correct, it is true that it gets to the point of compexity
> > where it seems that checking the proof is not just a matter of
> > mchanically checking derivation steps, but requires extra ingenuity.
> >
> > Now, HoTT, regarded as an internal language, shares with the concept
> > of derivators the potential to make much of this somewhat
> > messy-looking simplicial infinity-category theory become more
> > transparent and systematic, more mechanical. Therefore it might be
> > argued to be a little be backwards to try to force that messy
> > simplicial technology to realize itself inside HoTT. It might be
> > missing the golden opportunity to turn this around and use the
> > synthetic reasong.
> >
> > There is now one person, Felix Wellen, working on formalizing some
> > first basics of geometric representation theory within differentially
> > cohesion HoTT. I think it's a topic with plenty of opportunity.
> >
> > Best wishes,
> > urs
>
> --
> 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 HomotopyTypeThe...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.
>

[-- Attachment #2: Type: text/html, Size: 5075 bytes --]

Re: [HoTT] What is UF, what is HoTT and what is a univalent type theory?

[Vladimir Voevodsky]

[-- Attachment #1.1: Type: text/plain, Size: 5588 bytes --]

When one gives a false mathematical statement I can call it false.

When the statement itself is not mathematical and I believe it to be intentionally misleading I call it a lie. In this particular case it is possible that I was wrong, in which case I apologize.

I did not notice that the statement was about *a* class of categories.

It might be the case that geometric representation theorists care about *some* class of (infty,1)-categories that can be obtained by adding "a certain adjoint triple of modal operators” to HoTT (whatever that means).

In any case the sentence in question is not a mathematical statement and includes a reference to whether or not a certain group of people cares about something.

Vladimir.


> On Jun 6, 2016, at 10:32 AM, David Roberts <drobert...@gmail.com> wrote:
> 
> Dear Vladimir,
> 
> Please see Charles Rezk's work on globally equivariant homotopy theoretic models of cohesion. It is not something out of Urs' imagination.
> 
> Also, if something is false, call it false, not a 'lie', and provide a mathematical basis for such a statement.
> 
> Best regards,
> David
> 
> On 6 Jun 2016 4:45 pm, "Vladimir Voevodsky" <vlad...@ias.edu <mailto:vlad...@ias.edu>> wrote:
> Dear Urs,
> 
> > For instance a class of (infinity,1)-categories that geometric
> > representation theorists care about is neatly obtained in HoTT by just
> > adding a certain adjoint triple of modal operators (differential
> > cohesion)
> 
> this is a lie.
> 
> Geometric representation theorists care about the (infty,1)-categories that corresponds to different groups and to their interaction with each other. They care not about sitting inside one universal (infty,1)-category.
> 
> Vladimir.
> 
> 
> 
> 
> 
> > On Jun 4, 2016, at 9:11 AM, Urs Schreiber <urs.sc...@googlemail.com <mailto:urs.sc...@googlemail.com>> wrote:
> >
> >> They don’t take us seriously so far because we can not define
> >> (infty,1)-categories.
> >
> > The good news is, without even having to define them, HoTT already is
> > the internal language of certain (infinity,1)-categories. Which ones
> > precisely depends on which axioms are added or omitted.
> >
> > For instance a class of (infinity,1)-categories that geometric
> > representation theorists care about is neatly obtained in HoTT by just
> > adding a certain adjoint triple of modal operators (differential
> > cohesion) This yields a synthetic axiomatization of the homotopy
> > theory of D-modules and their representation theory, which is what is
> > mostly meant by "geometric representation theory".
> >
> > This route is the homotopy version of Lawvere's seminal vision of all
> > mathematics taking place synthetically inside a suitable elementary
> > topos. It's slightly ironic that this route is not more popular.
> > Because over in the community of ordinary (i.e. non-type theoretic)
> > infinity-category theory, there is the nagging feeling that handling
> > all those incarnations of infinity categories as simplicial and n-fold
> > simplicial objects from the outside may be rather inefficient for
> > deriving results. In order to overcome this there is the work on
> > derivators and the work by Riehl-Verity.
> >
> > A colleague of mine championing derivators praises the fact that they
> > offer him a formal way to verify the simplicial reasoning in work by
> > Lurie et al, which he finds intricate to the point of being
> > unverifiable to him. This certainly applies to other people, too.
> >
> > To check this, you should do a survey among your colleagues whether or
> > not they think that Lurie actually gave a proof of the cobordism
> > hypothesis. Lurie gives an intriciate argument in terms of
> > infinity-categories modeled on simplicial set, and while I fully trust
> > that it is correct, it is true that it gets to the point of compexity
> > where it seems that checking the proof is not just a matter of
> > mchanically checking derivation steps, but requires extra ingenuity.
> >
> > Now, HoTT, regarded as an internal language, shares with the concept
> > of derivators the potential to make much of this somewhat
> > messy-looking simplicial infinity-category theory become more
> > transparent and systematic, more mechanical. Therefore it might be
> > argued to be a little be backwards to try to force that messy
> > simplicial technology to realize itself inside HoTT. It might be
> > missing the golden opportunity to turn this around and use the
> > synthetic reasong.
> >
> > There is now one person, Felix Wellen, working on formalizing some
> > first basics of geometric representation theory within differentially
> > cohesion HoTT. I think it's a topic with plenty of opportunity.
> >
> > Best wishes,
> > urs
> 
> --
> 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 HomotopyTypeThe...@googlegroups.com <mailto:HomotopyTypeTheo...@googlegroups.com>.
> For more options, visit https://groups.google.com/d/optout <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 HomotopyTypeThe...@googlegroups.com <mailto:HomotopyTypeThe...@googlegroups.com>.
> For more options, visit https://groups.google.com/d/optout <https://groups.google.com/d/optout>.


[-- Attachment #1.2: Type: text/html, Size: 7865 bytes --]

[-- Attachment #2: Message signed with OpenPGP using GPGMail --]
[-- Type: application/pgp-signature, Size: 507 bytes --]

Re: [HoTT] What is UF, what is HoTT and what is a univalent type theory?

[David Roberts]

[-- Attachment #1: Type: text/plain, Size: 6094 bytes --]

Hi again,

I should have provided a reference to Rezk's paper -- here is an nLab page
with a link and context:

https://ncatlab.org/nlab/show/Global+Homotopy+Theory+and+Cohesion

Some of the ideas go back to Henriques-Gepner, and before that Elmendorf
and presumably others, but I'm not intimately familiar with the history. So
they are not plucked from the air, but fit into a more recent framework
with an explicitly \infty-topos-theoretic slant. That's all I can say for
now.

Best regards,
David
On 6 Jun 2016 8:26 pm, "Vladimir Voevodsky" <vlad...@ias.edu> wrote:

> When one gives a false mathematical statement I can call it false.
>
> When the statement itself is not mathematical and I believe it to be
> intentionally misleading I call it a lie. In this particular case it is
> possible that I was wrong, in which case I apologize.
>
> I did not notice that the statement was about *a* class of categories.
>
> It might be the case that geometric representation theorists care about
> *some* class of (infty,1)-categories that can be obtained by adding "a
> certain adjoint triple of modal operators” to HoTT (whatever that means).
>
> In any case the sentence in question is not a mathematical statement and
> includes a reference to whether or not a certain group of people cares
> about something.
>
> Vladimir.
>
>
> On Jun 6, 2016, at 10:32 AM, David Roberts <drobert...@gmail.com>
> wrote:
>
> Dear Vladimir,
>
> Please see Charles Rezk's work on globally equivariant homotopy theoretic
> models of cohesion. It is not something out of Urs' imagination.
>
> Also, if something is false, call it false, not a 'lie', and provide a
> mathematical basis for such a statement.
>
> Best regards,
> David
> On 6 Jun 2016 4:45 pm, "Vladimir Voevodsky" <vlad...@ias.edu> wrote:
>
>> Dear Urs,
>>
>> > For instance a class of (infinity,1)-categories that geometric
>> > representation theorists care about is neatly obtained in HoTT by just
>> > adding a certain adjoint triple of modal operators (differential
>> > cohesion)
>>
>> this is a lie.
>>
>> Geometric representation theorists care about the (infty,1)-categories
>> that corresponds to different groups and to their interaction with each
>> other. They care not about sitting inside one universal (infty,1)-category.
>>
>> Vladimir.
>>
>>
>>
>>
>>
>> > On Jun 4, 2016, at 9:11 AM, Urs Schreiber <urs.sc...@googlemail.com>
>> wrote:
>> >
>> >> They don’t take us seriously so far because we can not define
>> >> (infty,1)-categories.
>> >
>> > The good news is, without even having to define them, HoTT already is
>> > the internal language of certain (infinity,1)-categories. Which ones
>> > precisely depends on which axioms are added or omitted.
>> >
>> > For instance a class of (infinity,1)-categories that geometric
>> > representation theorists care about is neatly obtained in HoTT by just
>> > adding a certain adjoint triple of modal operators (differential
>> > cohesion) This yields a synthetic axiomatization of the homotopy
>> > theory of D-modules and their representation theory, which is what is
>> > mostly meant by "geometric representation theory".
>> >
>> > This route is the homotopy version of Lawvere's seminal vision of all
>> > mathematics taking place synthetically inside a suitable elementary
>> > topos. It's slightly ironic that this route is not more popular.
>> > Because over in the community of ordinary (i.e. non-type theoretic)
>> > infinity-category theory, there is the nagging feeling that handling
>> > all those incarnations of infinity categories as simplicial and n-fold
>> > simplicial objects from the outside may be rather inefficient for
>> > deriving results. In order to overcome this there is the work on
>> > derivators and the work by Riehl-Verity.
>> >
>> > A colleague of mine championing derivators praises the fact that they
>> > offer him a formal way to verify the simplicial reasoning in work by
>> > Lurie et al, which he finds intricate to the point of being
>> > unverifiable to him. This certainly applies to other people, too.
>> >
>> > To check this, you should do a survey among your colleagues whether or
>> > not they think that Lurie actually gave a proof of the cobordism
>> > hypothesis. Lurie gives an intriciate argument in terms of
>> > infinity-categories modeled on simplicial set, and while I fully trust
>> > that it is correct, it is true that it gets to the point of compexity
>> > where it seems that checking the proof is not just a matter of
>> > mchanically checking derivation steps, but requires extra ingenuity.
>> >
>> > Now, HoTT, regarded as an internal language, shares with the concept
>> > of derivators the potential to make much of this somewhat
>> > messy-looking simplicial infinity-category theory become more
>> > transparent and systematic, more mechanical. Therefore it might be
>> > argued to be a little be backwards to try to force that messy
>> > simplicial technology to realize itself inside HoTT. It might be
>> > missing the golden opportunity to turn this around and use the
>> > synthetic reasong.
>> >
>> > There is now one person, Felix Wellen, working on formalizing some
>> > first basics of geometric representation theory within differentially
>> > cohesion HoTT. I think it's a topic with plenty of opportunity.
>> >
>> > Best wishes,
>> > urs
>>
>> --
>> 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 HomotopyTypeThe...@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 HomotopyTypeThe...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.
>
>
>

[-- Attachment #2: Type: text/html, Size: 7708 bytes --]

Re: [HoTT] Re: What is UF, what is HoTT and what is a univalent type theory?

[Martin Escardo]

Thanks, Vladimir for this. It is good to know where you come from, 
explicitly, and what your philosophy and program are.

I will concentrate in one aspect of your reply, which is probably the 
one you didn't intend to emphasize:

On 03/06/16 13:49, Vladimir Voevodsky wrote:
> However the original philosophy of MLTT and the original philosophy of
> UF are different and our use of MLTT for UF is in a sense an abuse of
> the MLTT as Per himself politely mentioned a number of times.

Precisely.

It always seemed to me, for a long time, since the last millemium, that 
the identity type was ad hoc, starting from the fact that there were 
three alternative approaches to patch it:

(1) (Going back to Bishop) Work with setoids.

Perhaps this is *the* philosophy ML had in mind. I don't know. However, 
it is a pity that a formal system supporting this philosophy was 
created, but the philosophy was not formalised by Martin-Loef. But 
Martin Hofmann did this (excluding the universe). Is that what 
Martin-Lof had in mind?

(2) Have the reflection rule. Martin-Loef had this for a while.

But then how does this relate to (1)? I've never seen an account of 
this. People just concentrate on undecidability things regarding (2), 
which I think is a red hearing.

(3) Have the K axiom. This is due to Streicher.

Then UF has a fourth way to look at this:

(4) Certain types do satisfy the K axiom. But there is no reason why all 
types should satisfy it.

What worked as a "revelation" to me what not the univalence axiom (which 
makes (4) good), but something we can say before we consider the 
univalence axiom: although there is no reason to suppose that, in MLTT, 
any two points of Id X x y are themselves Id-related, we have that any 
two points of Sigma(y:X). Id x y are Id-related.

This was known before UF/HoTT, and was considered puzzling for a while. 
What is interesting is that homotopy explains this very clearly and 
naturally. It was this that convinced me that the homotopical view of 
types is correct, once one has identity types. It was not the univalence 
axiom or higher inductive types.

The identity type seemed something at the same time natural and weird 
from the point of view of the philosophy of the last millenium. Without 
changing MLTT, but now looking at it from the homotopical point of view, 
it seems now completely natural to me. Before it felt rather weird.

There is more to say, but I prefer this message to have just one point.

Martin

Re: [HoTT] What is UF, what is HoTT and what is a univalent type theory?

[Martin Escardo]

On 04/06/16 12:43, Michael Shulman wrote:
> On Thu, Jun 2, 2016 at 4:29 PM, Martin Escardo <m.es...@cs.bham.ac.uk> wrote:
>> The difference with
>> HoTT is that in HoTT such distinctions are merely axiomatized.
>
> Please stop saying this.  Obviously I can't claim to personally
> "define HoTT" in the same way that Vladimir can "define UF", but the
> term "homotopy type theory" as it is used, not just by me but by
> plenty of other people, DOES NOT refer only to the type theory
> described in the book that adds axioms to MLTT.  It INCLUDES cubical
> type theory.  If you want to refer to the formal type theory used in
> the book, some possibilities are "HoTT 1.0" or "Book HoTT".

I am happy to stop saying this.

I am glad that Vladimir said explicitly what he thinks UF is/should be 
(and that also he said more than I asked).

Perhaps you should say what you think HoTT is, for instance to prevent 
me from mis-representing it.

But also to prevent people from reading the book in an unintended way.

What is clear, both with UF and with HoTT, is that they are both 
(indended to be) a philosophy and also something mathematically precise 
matching such philosophy.

Perhaps each of them also explicitly desire some amount of vagueness, or 
open-endedness, or generality, e.g. to accommodate cubicaltt.

To make a parallel (again), I very much like intuitionistic mathematics 
as Brouwer initiated it. What we nowadays distil from it is called 
intuitionistic logic.

But with Brouwer it had a heavy amount of topology, which we now 
consider to be still very interesting (and in particular I do myself), 
but we don't any more consider to be the essence of intuitionistic 
mathematics.

I think I am in a similar process regarding UF/HoTT.

What I think happened was that with Brouwer, Heyting, Curry, Howard, de 
Brujin, Martin-Loef and many others,  and with topos theory too, we 
understood logic rather well, excluding equality.

Then Martin-Loef said something new about equality in the form of the 
identity type.

Like with topology in Brouwer's hands to understand logic, homotopy has 
been used to understand Martin-Loef identity. (Or, if you come from the 
other side, Martin-Loef identity has been used to formalize homotopy 
equivalence, but this is a later development (and certainly interesting, 
as I said in my previous message).)

But to say homotopy is the ultimate understanding of identity would be 
like saying that topology is the ultimate understanding of 
intuitionistic logic.

I do think that topology is a very good and precise understanding of 
intuitionistic logic, and that homotopy is a very good and precise 
understanding of identity.

However, I wouldn't like to refer to intuitionistic logic as topological 
logic, or to refer to a type theory with the identity type as homotopy 
type theory.

And the univalence axiom and higher-inductive types make sense on their 
own before we consider any homotopical interpretation, just as 
intuitionistic logic makes sense before we consider any topological 
interpretation.

Having said that, yes, I love both the topological and the homotopical 
interpretations of (mathematics and) logic, and, moreover, I would like 
to see them properly combined, as we discussed earlier.

Best,
Martin

Re: [HoTT] What is UF, what is HoTT and what is a univalent type theory?

[Martín Hötzel Escardó]

Many thanks, Mike, for your reply. I am prepared to agree with all your 
points, in particular:

(1) You use geometric logic to explain the gap between topology and 
intuitionistic logic in a very nice and precise way. In particular, you 
said "the rules of intuitionistic logic do not encompass a definition of 
topological space (though one might argue that the rules of *geometric* 
logic do)". Nice way to put it.

(2) You make the point that, since the presence of identity types makes 
types into infty-groupoids, we get (an incarnation of) homotopy theory. 
So, in this sense, yes, we have a much more precise match.

(But, to play devil's advocate, we do have a precise definition of 
geometry logic to match up with intuitionistic logic, but are you 
offering precise definitions of the things to be matched up in (2)? 
(Existing or to be developed.))

You also make a point that HoTT is not tied to a particular type theory, 
like Vladimir says UF is not tied to a particular type theory. I agree 
with this, and I am sorry if in previous messages I may have conveyed 
the opposite view.

Now, for the sake of discussion, suppose a particular incarnation of 
HoTT like in the book, based on MLTT. I wonder what you think about the 
question of when MLTT ends and HoTT begins. For instance, much of 
HoTT/UF works without anything added to MLTT, not even function 
extensionality, like seeing that types are infty-groupoids, the 
definition of n-type, the definition of equivalence and more. Is HoTT a 
way to understand (the identity types of) MLTT? (Which, in this case, 
is, as Vladimir said, not the originally intended one.)

Best,
Martin

On 08/06/16 09:18, Michael Shulman wrote:
> On Sun, Jun 5, 2016 at 1:40 PM, Martin Escardo <m.es...@cs.bham.ac.uk> wrote:
>> Perhaps you should say what you think HoTT is, for instance to prevent me
>> from mis-representing it.
>
> Personally (all caveats repeated), I prefer to use it for the
> mathematical subject involving the interaction of homotopy-theoretic
> and type-theoretic ideas, including models of type theory in classical
> homotopy theories but also application of homotopy-theoretic ideas to
> type theory.  I don't mean to specify any particular philosophy or
> motivation for doing such mathematics.
>
>> But also to prevent people from reading the book in an unintended way.
>
> Yes, it would be nice for the book to make clearer that the particular
> type theory used therein is only one possible choice, and other
> possibilities are a field of active research.
>
>> To make a parallel (again), I very much like intuitionistic mathematics as
>> Brouwer initiated it. What we nowadays distil from it is called
>> intuitionistic logic.
>>
>> But with Brouwer it had a heavy amount of topology, which we now consider to
>> be still very interesting (and in particular I do myself), but we don't any
>> more consider to be the essence of intuitionistic mathematics.
>>
>> ...
>>
>> But to say homotopy is the ultimate understanding of identity would be like
>> saying that topology is the ultimate understanding of intuitionistic logic.
>
> This is a very interesting point; I am glad that you brought it up.
> When you first mentioned it a while ago, my reaction was that
> "logically it makes sense, but intuitively it feels wrong".  But I
> didn't say that out loud because it didn't seem like a very good
> argument!  (-:
>
> After mulling it over for a while, however, I have a couple of real
> points to make, to explain my intuitive reaction.
>
> Firstly, I agree that topology is not the ultimate understanding of
> intuitionistic logic.  But I think one might more plausibly argue that
> topology is the ultimate understanding of *geometric* logic.  That is,
> the relationship between topology and intuitionistic logic is the same
> as the relationship between frames and Heyting algebras.  Every frame
> is a Heyting algebra, so topology furnishes models of intuitionistic
> logic.  But frame homomorphisms are different from Heyting algebra
> homomorphisms, and moreover not every Heyting algebra is complete; so
> there is more to intuitionistic logic than topology.
>
> So this is one concrete way in which I think the connection between
> homotopy and identity is closer than the connection between topology
> and intuitionistic logic.
>
> Secondly, I *DO* actually believe that homotopy is the ultimate
> understanding of identity.  Why?  That is essentially the definition
> of "homotopy"!  Homotopy theory is the study of infty-groupoids, and
> an infty-groupoid is exactly what you get when you take a vague
> intuitive notion of "collection" and allow "different witnesses of
> identity" in a coherent way.  The historical origins (and current
> concrete incarnations) of homotopy theory in topological spaces and
> simplicial sets are, philosophically, irrelevant; what the homotopy
> theorist is actually interested in are infty-groupoids, as witnessed
> by the tide sweeping homotopy theory into (infty,1)-categorical
> language that talks more directly about its objects of interest.
>
> A mathematical expression of this is Brunerie's observation that
> Martin-Lof's rule for identity types is essentially a definition of
> infty-groupoid, and that the definition one gets is essentially the
> very first such definition given by Grothendieck.  There is nothing
> analogous on the other side of your analogy: the rules of
> intuitionistic logic do not encompass a definition of topological
> space (though one might argue that the rules of *geometric* logic do).
>
> Best,
> Mike
>

-- 
http://www.cs.bham.ac.uk/~mhe

Re: [HoTT] What is UF, what is HoTT and what is a univalent type theory?

[Michael Shulman]

No, I am not offering precise definitions of the things to be matched
up in (2).  I don't think this detracts much from the point, given the
youth of the subject.  (-:

As for when MLTT ends and when HoTT begins, if "MLTT" and "HoTT" refer
to specific formal systems, then the answer is that HoTT begins
whenever we use something present in HoTT that is not present in MLTT,
like univalence or HITs.  But if "MLTT" and "HoTT" refer to
philosophies, attitudes, or techniques, then there's no reason that
one of them has to end at the same time as the other begins.  I would
say that HoTT begins whenever we start using ideas from homotopy
theory, including things like the definition of n-type and the
definition of equivalence that don't use anything added to the formal
system of MLTT.  Whether MLTT has ended before that depends on what
exactly the philosophy/attitude/techniques of MLTT mean, which I'm
probably not qualified to comment on.

Mike

On Wed, Jun 8, 2016 at 3:14 AM, Martín Hötzel Escardó
<m.es...@cs.bham.ac.uk> wrote:
> Many thanks, Mike, for your reply. I am prepared to agree with all your
> points, in particular:
>
> (1) You use geometric logic to explain the gap between topology and
> intuitionistic logic in a very nice and precise way. In particular, you said
> "the rules of intuitionistic logic do not encompass a definition of
> topological space (though one might argue that the rules of *geometric*
> logic do)". Nice way to put it.
>
> (2) You make the point that, since the presence of identity types makes
> types into infty-groupoids, we get (an incarnation of) homotopy theory. So,
> in this sense, yes, we have a much more precise match.
>
> (But, to play devil's advocate, we do have a precise definition of geometry
> logic to match up with intuitionistic logic, but are you offering precise
> definitions of the things to be matched up in (2)? (Existing or to be
> developed.))
>
> You also make a point that HoTT is not tied to a particular type theory,
> like Vladimir says UF is not tied to a particular type theory. I agree with
> this, and I am sorry if in previous messages I may have conveyed the
> opposite view.
>
> Now, for the sake of discussion, suppose a particular incarnation of HoTT
> like in the book, based on MLTT. I wonder what you think about the question
> of when MLTT ends and HoTT begins. For instance, much of HoTT/UF works
> without anything added to MLTT, not even function extensionality, like
> seeing that types are infty-groupoids, the definition of n-type, the
> definition of equivalence and more. Is HoTT a way to understand (the
> identity types of) MLTT? (Which, in this case, is, as Vladimir said, not the
> originally intended one.)
>
> Best,
> Martin
>
>
> On 08/06/16 09:18, Michael Shulman wrote:
>>
>> On Sun, Jun 5, 2016 at 1:40 PM, Martin Escardo <m.es...@cs.bham.ac.uk>
>> wrote:
>>>
>>> Perhaps you should say what you think HoTT is, for instance to prevent me
>>> from mis-representing it.
>>
>>
>> Personally (all caveats repeated), I prefer to use it for the
>> mathematical subject involving the interaction of homotopy-theoretic
>> and type-theoretic ideas, including models of type theory in classical
>> homotopy theories but also application of homotopy-theoretic ideas to
>> type theory.  I don't mean to specify any particular philosophy or
>> motivation for doing such mathematics.
>>
>>> But also to prevent people from reading the book in an unintended way.
>>
>>
>> Yes, it would be nice for the book to make clearer that the particular
>> type theory used therein is only one possible choice, and other
>> possibilities are a field of active research.
>>
>>> To make a parallel (again), I very much like intuitionistic mathematics
>>> as
>>> Brouwer initiated it. What we nowadays distil from it is called
>>> intuitionistic logic.
>>>
>>> But with Brouwer it had a heavy amount of topology, which we now consider
>>> to
>>> be still very interesting (and in particular I do myself), but we don't
>>> any
>>> more consider to be the essence of intuitionistic mathematics.
>>>
>>> ...
>>>
>>> But to say homotopy is the ultimate understanding of identity would be
>>> like
>>> saying that topology is the ultimate understanding of intuitionistic
>>> logic.
>>
>>
>> This is a very interesting point; I am glad that you brought it up.
>> When you first mentioned it a while ago, my reaction was that
>> "logically it makes sense, but intuitively it feels wrong".  But I
>> didn't say that out loud because it didn't seem like a very good
>> argument!  (-:
>>
>> After mulling it over for a while, however, I have a couple of real
>> points to make, to explain my intuitive reaction.
>>
>> Firstly, I agree that topology is not the ultimate understanding of
>> intuitionistic logic.  But I think one might more plausibly argue that
>> topology is the ultimate understanding of *geometric* logic.  That is,
>> the relationship between topology and intuitionistic logic is the same
>> as the relationship between frames and Heyting algebras.  Every frame
>> is a Heyting algebra, so topology furnishes models of intuitionistic
>> logic.  But frame homomorphisms are different from Heyting algebra
>> homomorphisms, and moreover not every Heyting algebra is complete; so
>> there is more to intuitionistic logic than topology.
>>
>> So this is one concrete way in which I think the connection between
>> homotopy and identity is closer than the connection between topology
>> and intuitionistic logic.
>>
>> Secondly, I *DO* actually believe that homotopy is the ultimate
>> understanding of identity.  Why?  That is essentially the definition
>> of "homotopy"!  Homotopy theory is the study of infty-groupoids, and
>> an infty-groupoid is exactly what you get when you take a vague
>> intuitive notion of "collection" and allow "different witnesses of
>> identity" in a coherent way.  The historical origins (and current
>> concrete incarnations) of homotopy theory in topological spaces and
>> simplicial sets are, philosophically, irrelevant; what the homotopy
>> theorist is actually interested in are infty-groupoids, as witnessed
>> by the tide sweeping homotopy theory into (infty,1)-categorical
>> language that talks more directly about its objects of interest.
>>
>> A mathematical expression of this is Brunerie's observation that
>> Martin-Lof's rule for identity types is essentially a definition of
>> infty-groupoid, and that the definition one gets is essentially the
>> very first such definition given by Grothendieck.  There is nothing
>> analogous on the other side of your analogy: the rules of
>> intuitionistic logic do not encompass a definition of topological
>> space (though one might argue that the rules of *geometric* logic do).
>>
>> Best,
>> Mike
>>
>
> --
> http://www.cs.bham.ac.uk/~mhe
>
>
> --
> 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 HomotopyTypeThe...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.

Re: [HoTT] What is UF, what is HoTT and what is a univalent type theory?

[Martin Escardo]

Mike, I think we agree a lot. So let me disagree here:

On 14/06/16 22:46, Michael Shulman wrote:
> As for when MLTT ends and when HoTT begins, if "MLTT" and "HoTT" refer
> to specific formal systems, then the answer is that HoTT begins
> whenever we use something present in HoTT that is not present in MLTT,
> like univalence or HITs.

I disagree, because, as I said in the previous messages in this thread, 
before we have univalence or HIT's, we can:

0. Know that types are omega-groupoids. (And you asserted that too.)

1. Define what an n-type is.

2. Define what an equivalence is.

3. Formulate the univalence axiom without asserting it (which is much 
subtler than it seems, as you know, because, for example, if in its 
formulation you use "isomorphism" rather than equivalence, then you get 
something that is provably false even before we begin looking for a model).

4. Blah blah blah.

In particular, the PhD thesis of my student Chuangjie Xu was based on 
this rationale, without ever invoking univalence or HIT's, even though 
is had *nothing* to do with homotopy.

We just saw that the new ideas about MLTT coming from homotopy were 
rather useful for what we wanted to talk about (Brouwerian continuity 
axioms and Kleene-Kreisel functionals).

Martin
(I still don't know where MLTT ends and HoTT begins.)

Re: [HoTT] What is UF, what is HoTT and what is a univalent type theory?

[Michael Shulman]

Note that the sentence you quoted began with "if MLTT and HoTT refer
to specific formal systems".  However, as I've been saying, I *don't*
think "HoTT" should refer to a specific formal system, and you've just
given one good argument as to why.  (-:

However, I suppose even on the grounds of formal systems one could
object.  ZF includes Zermelo set theory as a subsystem, but there's no
reason to say that ZF only "begins" when we start using the
replacement axiom.  So maybe it would be better to say that, as formal
systems, MLTT ends when we start using univalence/HITs/etc., but since
HoTT includes MLTT it begins at the same place.


On Tue, Jun 14, 2016 at 3:15 PM, Martin Escardo <m.es...@cs.bham.ac.uk> wrote:
> Mike, I think we agree a lot. So let me disagree here:
>
> On 14/06/16 22:46, Michael Shulman wrote:
>>
>> As for when MLTT ends and when HoTT begins, if "MLTT" and "HoTT" refer
>> to specific formal systems, then the answer is that HoTT begins
>> whenever we use something present in HoTT that is not present in MLTT,
>> like univalence or HITs.
>
>
> I disagree, because, as I said in the previous messages in this thread,
> before we have univalence or HIT's, we can:
>
> 0. Know that types are omega-groupoids. (And you asserted that too.)
>
> 1. Define what an n-type is.
>
> 2. Define what an equivalence is.
>
> 3. Formulate the univalence axiom without asserting it (which is much
> subtler than it seems, as you know, because, for example, if in its
> formulation you use "isomorphism" rather than equivalence, then you get
> something that is provably false even before we begin looking for a model).
>
> 4. Blah blah blah.
>
> In particular, the PhD thesis of my student Chuangjie Xu was based on this
> rationale, without ever invoking univalence or HIT's, even though is had
> *nothing* to do with homotopy.
>
> We just saw that the new ideas about MLTT coming from homotopy were rather
> useful for what we wanted to talk about (Brouwerian continuity axioms and
> Kleene-Kreisel functionals).
>
> Martin
> (I still don't know where MLTT ends and HoTT begins.)
>

Re: [HoTT] What is UF, what is HoTT and what is a univalent type theory?

[Martin Escardo]

On 14/06/16 23:30, Michael Shulman wrote:
> Note that the sentence you quoted began with "if MLTT and HoTT refer
> to specific formal systems".  However, as I've been saying, I *don't*
> think "HoTT" should refer to a specific formal system, and you've just
> given one good argument as to why.  (-:

After 50 minutes of reflection, I am not sure how to react to this. 
Whatever the formal system, univalent foundations does start by working 
in a type theory in which types are omega-groupoids and in which there 
is a notion of equivalence which is used to formulate univalence, which 
is postulated.

So I am not sure what you are up to here. Perhaps MLTT was wrong for 
this (univalence). Fair enough. But then we have cubicaltt, which 
accomplishes this and more.

Anyway, I am not sure what is the point you wanted to make.

I am happy for you not to commit yourself to a particular type theory, 
or any theory, but at some point you have to be sufficiently precise 
about what you want to talk about.

> However, I suppose even on the grounds of formal systems one could
> object.  ZF includes Zermelo set theory as a subsystem, but there's no
> reason to say that ZF only "begins" when we start using the
> replacement axiom.  So maybe it would be better to say that, as formal
> systems, MLTT ends when we start using univalence/HITs/etc., but since
> HoTT includes MLTT it begins at the same place.

I guess my point is that MLTT is naturally invariant under equivalence, 
before we postulate the univalence axiom.

In fact, the consistency of the univalence axiom says something about 
MLTT without the univalence axiom: namely that it can't distinguish 
equivalent types.

Martin

Re: [HoTT] What is UF, what is HoTT and what is a univalent type theory?

[Michael Shulman]

The main point I meant to make is that I don't know what you mean by
the question "where does MLTT end and HoTT begin?"  I think it could
mean different things, and have different answers, depending on
exactly what one means by "MLTT" and "HoTT" (let alone "begin" and
"end").

But I think this discussion has probably passed the point of
diminishing returns for a mailing list.  (-:  I would be happy to
continue privately if you like.

On Tue, Jun 14, 2016 at 4:33 PM, Martin Escardo <m.es...@cs.bham.ac.uk> wrote:
>
>
> On 14/06/16 23:30, Michael Shulman wrote:
>>
>> Note that the sentence you quoted began with "if MLTT and HoTT refer
>> to specific formal systems".  However, as I've been saying, I *don't*
>> think "HoTT" should refer to a specific formal system, and you've just
>> given one good argument as to why.  (-:
>
>
> After 50 minutes of reflection, I am not sure how to react to this. Whatever
> the formal system, univalent foundations does start by working in a type
> theory in which types are omega-groupoids and in which there is a notion of
> equivalence which is used to formulate univalence, which is postulated.
>
> So I am not sure what you are up to here. Perhaps MLTT was wrong for this
> (univalence). Fair enough. But then we have cubicaltt, which accomplishes
> this and more.
>
> Anyway, I am not sure what is the point you wanted to make.
>
> I am happy for you not to commit yourself to a particular type theory, or
> any theory, but at some point you have to be sufficiently precise about what
> you want to talk about.
>
>> However, I suppose even on the grounds of formal systems one could
>> object.  ZF includes Zermelo set theory as a subsystem, but there's no
>> reason to say that ZF only "begins" when we start using the
>> replacement axiom.  So maybe it would be better to say that, as formal
>> systems, MLTT ends when we start using univalence/HITs/etc., but since
>> HoTT includes MLTT it begins at the same place.
>
>
> I guess my point is that MLTT is naturally invariant under equivalence,
> before we postulate the univalence axiom.
>
> In fact, the consistency of the univalence axiom says something about MLTT
> without the univalence axiom: namely that it can't distinguish equivalent
> types.
>
> Martin

Fwd: [HoTT] What is UF, what is HoTT and what is a univalent type theory?

[Michael Shulman]

Here is a message that didn't make it through to the list.


---------- Forwarded message ----------
From: Michael Shulman <shu...@sandiego.edu>
Date: Wed, Jun 8, 2016 at 1:18 AM
Subject: Re: [HoTT] What is UF, what is HoTT and what is a univalent
type theory?
To: Martin Escardo <m.es...@cs.bham.ac.uk>
Cc: "HomotopyT...@googlegroups.com" <HomotopyT...@googlegroups.com>


On Sun, Jun 5, 2016 at 1:40 PM, Martin Escardo <m.es...@cs.bham.ac.uk> wrote:
> Perhaps you should say what you think HoTT is, for instance to prevent me
> from mis-representing it.

Personally (all caveats repeated), I prefer to use it for the
mathematical subject involving the interaction of homotopy-theoretic
and type-theoretic ideas, including models of type theory in classical
homotopy theories but also application of homotopy-theoretic ideas to
type theory.  I don't mean to specify any particular philosophy or
motivation for doing such mathematics.

> But also to prevent people from reading the book in an unintended way.

Yes, it would be nice for the book to make clearer that the particular
type theory used therein is only one possible choice, and other
possibilities are a field of active research.

> To make a parallel (again), I very much like intuitionistic mathematics as
> Brouwer initiated it. What we nowadays distil from it is called
> intuitionistic logic.
>
> But with Brouwer it had a heavy amount of topology, which we now consider to
> be still very interesting (and in particular I do myself), but we don't any
> more consider to be the essence of intuitionistic mathematics.
>
> ...
>
> But to say homotopy is the ultimate understanding of identity would be like
> saying that topology is the ultimate understanding of intuitionistic logic.

This is a very interesting point; I am glad that you brought it up.
When you first mentioned it a while ago, my reaction was that
"logically it makes sense, but intuitively it feels wrong".  But I
didn't say that out loud because it didn't seem like a very good
argument!  (-:

After mulling it over for a while, however, I have a couple of real
points to make, to explain my intuitive reaction.

Firstly, I agree that topology is not the ultimate understanding of
intuitionistic logic.  But I think one might more plausibly argue that
topology is the ultimate understanding of *geometric* logic.  That is,
the relationship between topology and intuitionistic logic is the same
as the relationship between frames and Heyting algebras.  Every frame
is a Heyting algebra, so topology furnishes models of intuitionistic
logic.  But frame homomorphisms are different from Heyting algebra
homomorphisms, and moreover not every Heyting algebra is complete; so
there is more to intuitionistic logic than topology.

So this is one concrete way in which I think the connection between
homotopy and identity is closer than the connection between topology
and intuitionistic logic.

Secondly, I *DO* actually believe that homotopy is the ultimate
understanding of identity.  Why?  That is essentially the definition
of "homotopy"!  Homotopy theory is the study of infty-groupoids, and
an infty-groupoid is exactly what you get when you take a vague
intuitive notion of "collection" and allow "different witnesses of
identity" in a coherent way.  The historical origins (and current
concrete incarnations) of homotopy theory in topological spaces and
simplicial sets are, philosophically, irrelevant; what the homotopy
theorist is actually interested in are infty-groupoids, as witnessed
by the tide sweeping homotopy theory into (infty,1)-categorical
language that talks more directly about its objects of interest.

A mathematical expression of this is Brunerie's observation that
Martin-Lof's rule for identity types is essentially a definition of
infty-groupoid, and that the definition one gets is essentially the
very first such definition given by Grothendieck.  There is nothing
analogous on the other side of your analogy: the rules of
intuitionistic logic do not encompass a definition of topological
space (though one might argue that the rules of *geometric* logic do).

Best,
Mike